Expand description
Inductive families: Lean’s add_inductive, including nested-inductive elimination and
recursor generation.
The kernel is handed the family’s types and constructor types and derives everything else itself: parameter/index split, universe constraints, strict positivity, recursive and reflexive flags, large elimination, the K flag, and every recursor with its reduction rules. An export’s claimed inductive, constructor and recursor declarations are admitted only if they are identical to what was derived, so a recursor with a forged rule, a missing induction hypothesis or an unjustified K flag cannot enter the environment.