"Error: Large non-propositional inductive types must be in Type." but the inductive is not large with mutual inductives #15934
Labels
kind: bug
An error, flaw, fault or unintended behaviour.
part: inductives
Inductive types, fixpoints, etc.
With no annotation we do get foo and bar in Set, and annotating
Inductive foo:Set := ...
also works.The text was updated successfully, but these errors were encountered: