@[export lean_is_level_def_eq]

def Lean.Meta.isLevelDefEqAuxImpl : Level → Level → MetaM Bool

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.isLevelDefEqAuxImpl lhs.succ rhs.succ = Lean.Meta.isLevelDefEqAux lhs rhs