diff options
| -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. |