diff options
author | Matthieu Sozeau <mattam@mattam.org> | 2017-07-31 16:50:42 +0200 |
---|---|---|
committer | Matthieu Sozeau <mattam@mattam.org> | 2017-09-19 10:28:03 +0200 |
commit | c2b881aae9c71a34199d2c66282512f2bdb19cf6 (patch) | |
tree | 6adfba97a4ea4e6a148265ae2964f55d5026e266 /test-suite/success | |
parent | 8966c9241207b6f5d4ee38508246ee97ed006e72 (diff) |
test-suite: polymorphism
Diffstat (limited to 'test-suite/success')
-rw-r--r-- | test-suite/success/polymorphism.v | 26 |
1 files changed, 19 insertions, 7 deletions
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v index 488443de1..7eaafc354 100644 --- a/test-suite/success/polymorphism.v +++ b/test-suite/success/polymorphism.v @@ -165,10 +165,10 @@ Module binders. exact A. Defined. - Definition nomoreu@{i j | i < j} (A : Type@{i}) : Type@{j}. + Definition nomoreu@{i j | i < j +} (A : Type@{i}) : Type@{j}. pose(foo:=Type). exact A. - Fail Defined. + Fail Defined. Abort. Polymorphic Definition moreu@{i j +} (A : Type@{i}) : Type@{j}. @@ -178,16 +178,28 @@ Module binders. Check moreu@{_ _ _ _}. - Fail Definition morec@{i j| } (A : Type@{i}) : Type@{j} := A. + Fail Definition morec@{i j|} (A : Type@{i}) : Type@{j} := A. (* By default constraints are extensible *) - Definition morec@{i j} (A : Type@{i}) : Type@{j} := A. + Polymorphic Definition morec@{i j} (A : Type@{i}) : Type@{j} := A. + Check morec@{_ _}. - (* FIXME: not handled in proofs correctly yet *) + (* Handled in proofs as well *) Lemma bar@{i j | } : Type@{i}. exact Type@{j}. - Defined. - + Fail Defined. + Abort. + + Lemma bar@{i j| i < j} : Type@{j}. + Proof. + exact Type@{i}. + Qed. + + Lemma barext@{i j|+} : Type@{j}. + Proof. + exact Type@{i}. + Qed. + End binders. Section cats. |