Stream: Coq devs & plugin devs

Topic: inductive/constructor universe instance

Enrico Tassi (Oct 14 2020 at 20:12):

Can I assume that if t : I@{u1 .. un} for I universe polymorphic niductive, then if t is a constructor k it is k@{u1 .. un} ?
Do the inductive type and its constructor agree on universe instances?

Gaëtan Gilbert (Oct 14 2020 at 20:14):

if cumulative polymorphic then no
unless I misunderstand the question

Last updated: Oct 16 2021 at 02:03 UTC