Stream: Coq devs & plugin devs

Topic: Universe levels in inductive arity


view this post on Zulip Enrico Tassi (Jul 18 2022 at 10:21):

Am I right that non-uniform parameters do not contribute to the universe level of the inductive/constructor?

view this post on Zulip Gaƫtan Gilbert (Jul 18 2022 at 10:21):

yes


Last updated: Feb 06 2023 at 19:03 UTC