def Lean.Elab.Structural.withCommonTelescope {α : Type} (preDefs : Array PreDefinition) (k : Array Expr → Array Expr → M α) : 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 Expr → Array Expr → M α) (fvars vals : Array Expr) : M α

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

Equations

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

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

Equations

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