@[extern lean_mk_cases_on]

opaque Lean.mkCasesOnImp (env : Environment) (declName : Name) : Except KernelException Declaration

def Lean.mkCasesOn (declName : Name) : MetaM Unit

Equations

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