diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/cumulativity.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v index 0ee85712e2..303cd7146e 100644 --- a/test-suite/success/cumulativity.v +++ b/test-suite/success/cumulativity.v @@ -98,3 +98,13 @@ Section down. intros H f g Hfg. exact (H f g Hfg). Defined. End down. + +Record Arrow@{i j} := { arrow : Type@{i} -> Type@{j} }. + +Fail Definition arrow_lift@{i i' j j' | i' < i, j < j'} + : Arrow@{i j} -> Arrow@{i' j'} + := fun x => x. + +Definition arrow_lift@{i i' j j' | i' = i, j < j'} + : Arrow@{i j} -> Arrow@{i' j'} + := fun x => x. |