Documentation

Lean.Elab.PreDefinition.Structural.Main

def Lean.Elab.Structural.structuralRecursion (preDefs : Array Lean.Elab.PreDefinition) :

Lean.Elab.TermElabM Unit

Equations

Lean.Elab.structuralRecursion preDefs = if (Array.size preDefs != 1) = true then Lean.throwError (Lean.toMessageData "structural recursion does not handle mutually recursive functions") else do let discr ← liftM (Lean.Elab.Structural.run (Lean.Elab.Structural.elimRecursion (Array.getOp preDefs 0)) { addMatchers := #[] }) let x : (Nat × Lean.Elab.PreDefinition) × Lean.Elab.Structural.State := discr match x with | ((recArgPos, preDefNonRec), state) => do let preDefNonRec ← liftM (Lean.Elab.eraseRecAppSyntax preDefNonRec) let preDef ← liftM (Lean.Elab.eraseRecAppSyntax (Array.getOp preDefs 0)) Array.forM liftM state.addMatchers 0 (Array.size state.addMatchers) liftM (Lean.Elab.Structural.registerEqnsInfo preDef recArgPos) Lean.Meta.mapError (Lean.Elab.addNonRec preDefNonRec false) fun msg => Lean.toMessageData "structural recursion failed, produced type incorrect term" ++ Lean.toMessageData (Lean.indentD msg) ++ Lean.toMessageData "" Lean.Elab.addAndCompilePartialRec #[preDef] Lean.Elab.Structural.addSmartUnfoldingDef preDef recArgPos Lean.Elab.applyAttributesOf #[preDefNonRec] Lean.AttributeApplicationTime.afterCompilation