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)

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 (docCtx : LocalContext × LocalInstances) (preDefs : Array PreDefinition) (termMeasure?s : Array (Option TerminationMeasure)) : TermElabM Unit

Equations

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