Stream: Coq devs & plugin devs

Topic: inductive/constructor universe instance


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

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