RequireImport TestSuite.admit. Set Universe Polymorphism. Inductive paths {A : Type} (a : A) : A -> Type :=
idpath : paths a a.
Goalforall (A : Type) (P : forall _ : A, Type) (x0 : A)
(p : P x0) (q : @paths (@sigT A P) (@existT A P x0 p) (@existT A P x0 p)),
@paths (@paths (@sigT A P) (@existT A P x0 p) (@existT A P x0 p))
(@idpath (@sigT A P) (@existT A P x0 p))
(@idpath (@sigT A P) (@existT A P x0 p)). intros. induction q.
admit. Qed. (** Error: Illegal application: The term "paths_rect" of type "forall (A : Type) (a : A) (P : forall a0 : A, paths a a0 -> Type), P a (idpath a) -> forall (y : A) (p : paths a y), P y p" cannot be applied to the terms "{x : _ & P x}" : "Type" "s" : "{x : _ & P x}" "fun (a : {x : _ & P x}) (_ : paths s a) => paths (idpath a) (idpath a)" : "forall a : {x : _ & P x}, paths s a -> Type" "match proof_admitted return (paths (idpath s) (idpath s)) with end" : "paths (idpath s) (idpath s)" "s" : "{x : _ & P x}" "q" : "paths (existT P x0 p) (existT P x0 p)" The 3rd term has type "forall a : {x : _ & P x}, paths s a -> Type"
which should be coercible to "forall a : {x : _ & P x}, paths s a -> Type". *)
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.
