Documentation

Lean.Meta.LevelDefEq

source
@[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.