def
Lean.Elab.Structural.withCommonTelescope
{α : Type}
(preDefs : Array PreDefinition)
(k : Array Expr → Array Expr → M α)
:
M α
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Lean.Elab.Structural.structuralRecursion
(preDefs : Array PreDefinition)
(termMeasure?s : Array (Option TerminationMeasure))
:
Equations
- One or more equations did not get rendered due to their size.