Documentation

Lean.Elab.PreDefinition.WF.Main

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 a => a.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.