diff options
Diffstat (limited to 'test-suite/bugs/closed/6775.v')
-rw-r--r-- | test-suite/bugs/closed/6775.v | 43 |
1 files changed, 43 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/6775.v b/test-suite/bugs/closed/6775.v new file mode 100644 index 00000000..206df23b --- /dev/null +++ b/test-suite/bugs/closed/6775.v @@ -0,0 +1,43 @@ +(* Issue caused and fixed during the lifetime of #6775: unification + failing on partially applied cumulative inductives. *) + +Set Universe Polymorphism. + +Set Polymorphic Inductive Cumulativity. + +Unset Elimination Schemes. + +Inductive paths@{i} {A : Type@{i}} (a : A) : A -> Type@{i} := + idpath : paths a a. + +Arguments idpath {A a} , [A] a. + +Notation "x = y :> A" := (@paths A x y) : type_scope. +Notation "x = y" := (x = y :>_) : type_scope. + +Definition inverse {A : Type} {x y : A} (p : x = y) : y = x + := match p with idpath => idpath end. + +Arguments inverse {A x y} p : simpl nomatch. + +Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z := + match p, q with idpath, idpath => idpath end. + +Arguments concat {A x y z} p q : simpl nomatch. + +Notation "1" := idpath. + +Reserved Notation "p @ q" (at level 20). +Notation "p @ q" := (concat p q). + +Reserved Notation "p ^" (at level 3, format "p '^'"). +Notation "p ^" := (inverse p). + +Definition concat_pV_p {A} {x y z : A} (p : x = z) (q : y = z) : + (p @ q^) @ q = p + := + (match q as i return forall p, (p @ i^) @ i = p with + idpath => + fun p => + match p with idpath => 1 end + end) p. |