@[export lean_is_level_def_eq]

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

Equations

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