Documentation

Lean.Meta.LevelDefEq

source
@[export lean_is_level_def_eq]
def Lean.Meta.isLevelDefEqAuxImpl :
Level → Level → MetaM Bool
Equations
    Instances For