This module contains code common to mutual-via-fixedpoint constructions, i.e. well-founded recursion and partial fixed-points, but independent of the details of the mutual packing.

def Lean.Elab.Mutual.addPreDefsFromUnary (docCtx : LocalContext × LocalInstances) (preDefs preDefsNonrec : Array PreDefinition) (unaryPreDefNonRec : PreDefinition) (cacheProofs : Bool := true) : TermElabM Unit

def Lean.Elab.Mutual.cleanPreDef (preDef : PreDefinition) (cacheProofs : Bool := true) : MetaM PreDefinition

Cleans the right-hand-sides of the predefinitions, to prepare for inclusion in the EqnInfos:

• Remove RecAppSyntax markers
• Abstracts nested proofs (and for that, add the _unsafe_rec definitions)

def Lean.Elab.Mutual.addPreDefAttributes (preDefs : Array PreDefinition) : TermElabM Unit

Assign final attributes to the definitions. Assumes the EqnInfos to be already present.