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

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

def Lean.Elab.getFixedPrefix (preDefs : Array Lean.Elab.PreDefinition) : Lean.Elab.TermElabM Nat

Equations

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

def Lean.Elab.varyingVarNames (fixedPrefixSize : Nat) (preDef : Lean.Elab.PreDefinition) : Lean.MetaM (Array Lean.Name)

Collect the names of the varying variables (after the fixed prefix); this also determines the arity for the well-founded translations, and is turned into an ArgsPacker. We use the term to determine the arity, but take the name from the type, for better names in the

fun : (n : Nat) → Nat | 0 => 0 | n+1 => fun n

idiom.

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