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.withCommonTelescope {α : Type} (preDefs : Array PreDefinition) (k : Array Expr → Array Expr → MetaM α) : MetaM α

partial def Lean.Elab.Mutual.withCommonTelescope.go {α : Type} (k : Array Expr → Array Expr → MetaM α) (fvars vals : Array Expr) : MetaM α

def Lean.Elab.Mutual.addPreDefsFromUnary (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.