Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: bug_3911.v Sprache: Coq

Original von: 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
. *)

¤ Dauer der Verarbeitung: 0.20 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
Eigene Datei ansehen

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.