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: Nov 29 2023 at 18:01 UTC