Stream: Coq devs & plugin devs

Topic: Asserting an inductive is cumulative

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: Oct 08 2024 at 15:02 UTC