Module recursor 

R2 — auto-derived recursors (dependent eliminators) for inductive types.

Today a user who declares an inductive must hand-write the match/fix to recurse over it. Lean/Coq instead AUTO-GENERATE the recursor I.rec (the dependent eliminator) from the declaration, so “declare ℕ, get induction for free.” This module is that derivation: from an inductive’s registered constructors it synthesizes

I_rec : Π(P : I → Type). minor₀ → … → minorₖ → Π(x : I). P x
I_rec := λP. λf₀ … λfₖ. fix rec. λx. match x return (λx. P x) with
           | Cᵢ a… => fᵢ a… (rec aⱼ)…        -- one rec-call per recursive argument

where each minor premise is Π(args). Π(IH : P aⱼ for each recursive arg). P (Cᵢ args). The synthesized term is an ordinary kernel Term, so it is re-checked by infer_type for coverage + termination — and (the point of building it now) independently re-derived by the recheck second kernel. A Prop motive may be passed wherever the Type motive is expected, by cumulativity (Prop ≤ Type 0), so the single derived recursor serves BOTH computation and induction.

Scope: parametric AND indexed inductive families. Beyond the uniform PARAMETERS of a type like List A, an indexed family has INDICES that vary per constructor — Eq A x : A → Prop with refl : Eq A x x. Their eliminator’s motive abstracts over the indices, so derive_recursor("Eq") synthesizes FULL Paulin-Mohring J: Π(A). Π(x:A). Π(P : Π(y:A). Eq A x y → Sort). P x (refl A x) → Π(y). Π(h:Eq A x y). P y h — the identity eliminator as a kernel-checked term, not an axiom.

Functions

derive_recursor

Build I_rec’s term and type for the inductive ind. Returns (recursor_type, recursor_term) where recursor_type is exactly infer_type(recursor_term) — so the type is, by construction, the one the kernel certifies the term against.