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 α

Equations

• Lean.Elab.Mutual.withCommonTelescope preDefs k = Lean.Elab.Mutual.withCommonTelescope.go k #[] (Array.map (fun (x : Lean.Elab.PreDefinition) => x.value) preDefs)

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

Equations

• One or more equations did not get rendered due to their size.

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)

Equations

• Lean.Elab.Mutual.cleanPreDef preDef cacheProofs = do let preDef ← liftM (Lean.Elab.eraseRecAppSyntax preDef) let preDef ← Lean.Elab.abstractNestedProofs preDef cacheProofs pure preDef

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

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

Equations

• One or more equations did not get rendered due to their size.