def Lean.Meta.getSparseCasesOnEq (sparseCasesOnName : Name) : MetaM Name

Given a sparseCasesOn, creates an equational theorem for the else-case.

Equations

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