inductive List (a: Type): Type where| Good: List a| Good2: List a -> List a| Bad: List b -> List a ^^^^^^^ -- not allowed!- In hindsight, this makes sense, as the parameter really is a trick to represent, well, parametric polymorphism.
inductive List (a: Type): Type where| Good: List a| Good2: List a -> List a| Bad: List b -> List a ^^^^^^^ -- not allowed!