Documentation

Lean.Meta.LevelDefEq

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