Skip to main content

derive_rec_on

logicaffeine_kernel::recursor

Function derive_rec_on 

Source 
pub fn derive_rec_on(ctx: &Context, ind: &str) -> KernelResult<(Term, Term)>
Expand description

I_recOn — the eliminator with the MAJOR PREMISE moved in front of the minors, which is the argument order induction/match elaboration wants and the one every Lean development writes by hand.

Lean generates it at every declaration (Lean/Elab/Inductive.lean:729) by exactly this permutation (Lean/Meta/Constructions/RecOn.lean:20-31):

before: As Cs minor_premises indices major-premise
after:  As Cs indices major-premise minor_premises

It is a RESHAPING of derive_recursor’s answer and nothing else — every soundness gate (the motive-sort rule, strict positivity, the termination guard that admitted the Fix) is the one the eliminator already passed, and no new trusted code is added by moving binders.