Enrico Tassi (Nov 03 2020 at 18:48): Enrico Tassi (Nov 03 2020 at 18:48):I can check an inductive is polymoprhic by writing Check foo@{Type...}.
Is there a simple check (for a test suite) that foo is also cumulative?
Gaëtan Gilbert (Nov 03 2020 at 19:31):you can do something like
Section S. Set Universe Polymorphism. (* polymorphic univs in section disappear at the end of the section, so no side effects to doing the test *)
Universes i j. Constraint i < j. (* forbid unifying i and j *)
Check fun x : foo@{i} => x : foo@{j}.
End S.
(according to the cumulativity of foo)
after https://github.com/coq/coq/pull/12653 you can do
Fail Fail Inductive test@{+i} := C : foo@{i} -> test.
Last updated: Apr 20 2024 at 10:02 UTC