Stream: Coq devs & plugin devs

Topic: Asserting an inductive is cumulative


view this post on Zulip 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?

view this post on Zulip 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 16 2021 at 02:03 UTC