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

Equations

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

partial def Lean.Elab.withCommonTelescope.go {α : Type} (k : Array Lean.Expr → Array Lean.Expr → Lean.Elab.TermElabM α) (fvars : Array Lean.Expr) (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.wfRecursion (preDefs : Array Lean.Elab.PreDefinition) (wf? : Option Lean.Elab.WF.TerminationWF) (decrTactic? : Option Lean.Syntax) : Lean.Elab.TermElabM Unit

Equations

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