diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/cumulativity.v | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v index 3d97f27b16..31fed98952 100644 --- a/test-suite/success/cumulativity.v +++ b/test-suite/success/cumulativity.v @@ -137,3 +137,12 @@ Module WithIndex. Monomorphic Constraint i < j. Definition bar : eq mkfoo@{i} mkfoo@{j} := eq_refl _. End WithIndex. + +Module CumulApp. + + (* i is covariant here, and we have one parameter *) + Inductive foo@{i} (A : nat) : Type@{i+1} := mkfoo (B : Type@{i}). + + Definition bar@{i j|i<=j} := fun x : foo@{i} 0 => x : foo@{j} 0. + +End CumulApp. |