pub fn derive_cases_on(ctx: &Context, ind: &str) -> KernelResult<(Term, Term)>Expand description
I_casesOn — recOn with the INDUCTION HYPOTHESES dropped from every minor premise.
Lean’s is @Nat.casesOn : {motive : Nat → Sort u} → (t : Nat) → motive Nat.zero → ((n : Nat) → motive n.succ) → motive t: the case analysis cases h compiles to, and the
constant every match elaborates through. It is generated at every declaration
(Lean/Elab/Inductive.lean:730).
Derived here rather than built: each minor premise keeps its FIELD binders and loses its
ih binders, and the body hands the original eliminator a minor that ignores the hypotheses
it was given. So casesOn is rec with the recursion thrown away, which is exactly what it
means — and it inherits every gate rec passed rather than opening a second door.