def Lean.Elab.Structural.withCommonTelescope {α : Type} (preDefs : Array Lean.Elab.PreDefinition) (k : Array Lean.Expr → Array Lean.Expr → Lean.Elab.Structural.M α) : Lean.Elab.Structural.M α

Equations

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

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

def Lean.Elab.Structural.getMutualFixedPrefix (preDefs : Array Lean.Elab.PreDefinition) : Lean.Elab.Structural.M Nat

Equations

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

def Lean.Elab.Structural.reportTermArg (preDef : Lean.Elab.PreDefinition) (recArgPos : Nat) : Lean.MetaM Unit

Equations

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

def Lean.Elab.Structural.structuralRecursion (preDefs : Array Lean.Elab.PreDefinition) (termArg?s : Array (Option Lean.Elab.TerminationArgument)) : Lean.Elab.TermElabM Unit

Equations

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