Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Lean.Elab.Structural.structuralRecursion
(docCtx : LocalContext × LocalInstances)
(preDefs : Array PreDefinition)
(termMeasure?s : Array (Option TerminationMeasure))
:
Equations
- One or more equations did not get rendered due to their size.