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: Mar 29 2024 at 05:40 UTC