diff options
| author | Amin Timany | 2017-07-07 14:26:05 +0200 |
|---|---|---|
| committer | Amin Timany | 2017-07-31 18:05:54 +0200 |
| commit | 7f78827b3f8583a7c0e79a78266bc01a411ed818 (patch) | |
| tree | fe63107376abd5d18328a433e18356d752e17e1e /test-suite/success | |
| parent | fbe0b2645eab84012aec50e76d94e15a3fefe664 (diff) | |
Add test for NonCumulative inductives
Diffstat (limited to 'test-suite/success')
| -rw-r--r-- | test-suite/success/cumulativity.v | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v index 604da2108e..351d472a11 100644 --- a/test-suite/success/cumulativity.v +++ b/test-suite/success/cumulativity.v @@ -68,4 +68,16 @@ End subtyping_test. Record A : Type := { a :> Type; }. -Record B (X : A) : Type := { b : X; }.
\ No newline at end of file +Record B (X : A) : Type := { b : X; }. + +NonCumulative Inductive NCList (A: Type) + := ncnil | nccons : A -> NCList A -> NCList A. + +Section NCListLift. + Universe i j. + + Constraint i < j. + + Fail Definition LiftNCL {A} : NCList@{i} A -> NCList@{j} A := fun x => x. + +End NCListLift. |