Lean.Elab.PreDefinition.WF.Fix

Equations

Lean.Elab.WF.mkFix preDef wfRel decrTactic? = do let wfFix ← Lean.Meta.forallBoundedTelescope preDef.type (some 1) fun x type => let x := Array.getOp x 0; do let α ← liftM (Lean.Meta.inferType x) let u ← liftM (Lean.Meta.getLevel α) let v ← liftM (Lean.Meta.getLevel type) let motive ← liftM (Lean.Meta.mkLambdaFVars #[x] type false true) let rel : Lean.Expr := Lean.mkProj `WellFoundedRelation 0 wfRel let wf : Lean.Expr := Lean.mkProj `WellFoundedRelation 1 wfRel pure (Lean.mkApp4 (Lean.mkConst `WellFounded.fix [u, v]) α motive rel wf) let a ← liftM (Lean.Meta.inferType wfFix) let a ← liftM (Lean.Meta.whnf a) Lean.Meta.forallBoundedTelescope (Lean.Expr.bindingDomain! a) (some 2) fun xs x => let x := Array.getOp xs 0; let F := Array.getOp xs 1; let val := Lean.Expr.betaRev preDef.value #[x]; do let val ← Lean.Elab.WF.processSumCasesOn x F val fun x F val => Lean.Elab.WF.processPSigmaCasesOn x F val (Lean.Elab.WF.replaceRecApps preDef.declName decrTactic?) let a ← liftM (Lean.Meta.mkLambdaFVars #[x, F] val false true) pure { ref := preDef.ref, kind := preDef.kind, levelParams := preDef.levelParams, modifiers := preDef.modifiers, declName := preDef.declName, type := preDef.type, value := Lean.mkApp wfFix a }