def
Lean.Elab.wfRecursion
(preDefs : Array Lean.Elab.PreDefinition)
(wf? : Option Lean.Elab.WF.TerminationWF)
(decrTactic? : Option Lean.Syntax)
:
Equations
- Lean.Elab.wfRecursion preDefs wf? decrTactic? = do let unaryPreDef ← Lean.withoutModifyingEnv do let r ← forIn preDefs PUnit.unit fun preDef r => do liftM (Lean.Elab.addAsAxiom preDef) pure (ForInStep.yield PUnit.unit) let x : PUnit := r let unaryPreDefs ← liftM (Lean.Elab.WF.packDomain preDefs) liftM (Lean.Elab.WF.packMutual unaryPreDefs) let wfRel ← Lean.Elab.WF.elabWFRel preDefs unaryPreDef wf? let preDefNonRec ← Lean.withoutModifyingEnv do liftM (Lean.Elab.addAsAxiom unaryPreDef) Lean.Elab.WF.mkFix unaryPreDef wfRel decrTactic? let preDefNonRec ← liftM (Lean.Elab.eraseRecAppSyntax preDefNonRec) let cls : Lean.Name := `Elab.definition.wf let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.Elab.TermElabM Unit := fun y => do let preDefs ← Array.mapM (fun d => liftM (Lean.Elab.eraseRecAppSyntax d)) preDefs Lean.Elab.addNonRec preDefNonRec true Lean.Elab.addNonRecPreDefs preDefs preDefNonRec liftM (Lean.Elab.WF.registerEqnsInfo preDefs preDefNonRec.declName) let r ← forIn preDefs PUnit.unit fun preDef r => do Lean.Elab.applyAttributesOf #[preDef] Lean.AttributeApplicationTime.afterCompilation pure (ForInStep.yield PUnit.unit) let x : PUnit := r Lean.Elab.addAndCompilePartialRec preDefs if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData ">> " ++ Lean.toMessageData preDefNonRec.declName ++ Lean.toMessageData " :=\n" ++ Lean.toMessageData preDefNonRec.value ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y