diff options
author | Matthieu Sozeau <mattam@mattam.org> | 2018-03-08 07:38:33 -0300 |
---|---|---|
committer | Matthieu Sozeau <mattam@mattam.org> | 2018-03-08 07:40:49 -0300 |
commit | a7dc1040e4fbd3e996f411f6c0e46e74cae8c93b (patch) | |
tree | 740f2fecbbbce2d29455a06b8e688efc624dbdfe /test-suite/success | |
parent | ce87e338529f4dd174f1c870b83162bac6d2b9ae (diff) |
Add test-suite file for cumulative constructors
Diffstat (limited to 'test-suite/success')
-rw-r--r-- | test-suite/success/cumulativity.v | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v index e05762477..4dda36042 100644 --- a/test-suite/success/cumulativity.v +++ b/test-suite/success/cumulativity.v @@ -134,3 +134,24 @@ Definition withparams_co@{i i' j|i < i', i' < j} : withparams@{i j} -> withparam Fail Definition withparams_not_irr@{i i' j|i' < i, i' < j} : withparams@{i j} -> withparams@{i' j} := fun x => x. + +(** Cumulative constructors *) + + +Record twotys@{u v w} : Type@{w} := + twoconstr { fstty : Type@{u}; sndty : Type@{v} }. + +Monomorphic Universes i j k l. + +Monomorphic Constraint i < j. +Monomorphic Constraint j < k. +Monomorphic Constraint k < l. + +Parameter Tyi : Type@{i}. + +Definition checkcumul := + eq_refl _ : @eq twotys@{k k l} (twoconstr@{i j k} Tyi Tyi) (twoconstr@{j i k} Tyi Tyi). + +(* They can only be compared at the highest type *) +Fail Definition checkcumul' := + eq_refl _ : @eq twotys@{i k l} (twoconstr@{i j k} Tyi Tyi) (twoconstr@{j i k} Tyi Tyi). |