Quelle bug_3454.v Sprache: Coq

Set Primitive Projections.
Set Implicit Arguments.

Record prod {A} {B}:= pair { fst : A ; snd : B }.
Notation " A * B " := (@prod A B) : type_scope.
Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }.
Notation pr1 := (@projT1 _ _).
Arguments prod : clear implicits.

Check (@projT1 _ (fun x : nat => x = x)).
Check (fun s : @sigT nat (fun x : nat => x = x) => s.(projT1)).

Record rimpl {b : bool} {n : nat} := { foo : forall {x : nat}, x = n }.

Check (fun r : @rimpl true 0 => r.(foo) (x:=0)).
Check (fun r : @rimpl true 0 => @foo true 0 r 0).
Check (fun r : @rimpl true 0 => foo r (x:=0)).
Check (fun r : @rimpl true 0 => @foo _ _ r 0).
Check (fun r : @rimpl true 0 => r.(@foo _ _)).
Check (fun r : @rimpl true 0 => r.(foo)).

Notation "{ x : T & P }" := (@sigT T P).
Notation "{ x : A & P }" := (sigT (A:=A) (fun x => P)) : type_scope.
(* Notation "{ x : T * U  & P }" := (@sigT (T * U) P). *)

Definition compose {A B C : Type} (g : B -> C) (f : A -> B) := fun x => g (f x).
Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope.
Arguments idpath {A a} , [A] a.
Class IsEquiv {A B : Type} (f : A -> B) := {}.

Local Instance isequiv_tgt_compose A B
: @IsEquiv (A -> {xy : B * B & fst xy = snd xy})
           (A -> B)
           (@compose A {xy : B * B & fst xy = snd xy} B
                     (@compose {xy : B * B & fst xy = snd xy} _ B (@snd B B) pr1)) := {}.
(* Toplevel input, characters 220-223: *)
(* Error: Cannot infer this placeholder. *)

Local Instance isequiv_tgt_compose' A B
: @IsEquiv (A -> {xy : B * B & fst xy = snd xy})
           (A -> B)
           (@compose A {xy : B * B & fst xy = snd xy} B (@compose {xy : B * B & fst xy = snd xy} _ B (@snd _ _) pr1)) := {}.
(* Toplevel input, characters 221-232: *)
(* Error: *)
(* In environment *)
(* A : Type *)
(* B : Type *)
(* The term "pr1" has type "sigT ?30 -> ?29" while it is expected to have type *)
(*  "{xy : B * B & fst xy = snd xy} -> ?27 * B". *)

Local Instance isequiv_tgt_compose'' A B
: @IsEquiv (A -> {xy : B * B & fst xy = snd xy})
           (A -> B)
           (@compose A {xy : B * B & fst xy = snd xy} B (@compose {xy : B * B & fst xy = snd xy} _ B (@snd _ _)
                                                                  (fun s => s.(projT1)))) := {}.
(* Toplevel input, characters 15-241:
Error:
Cannot infer an internal placeholder of type "Type" in environment:

A : Type
B : Type
x : ?32
. *)

quality99%

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.