@[extern lean_mk_cases_on]

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

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

Equations

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