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: Dec 07 2023 at 07:39 UTC