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

Equations

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

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

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

Equations

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

def Lean.Elab.varyingVarNames (fixedPrefixSize : Nat) (preDef : PreDefinition) : MetaM (Array 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.

Equations

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

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

Equations

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