TorchLean API
Docs Home
Guide
Examples
Graphs
Lean
.
Meta
.
LevelDefEq
Search
Declaration colors
def
theorem
structure
axiom
return to top
source
Imports
Lean.Meta.DecLevel
Lean.Util.CollectMVars
Imported by
Lean
.
Meta
.
isLevelDefEqAuxImpl
source
@[export lean_is_level_def_eq]
def
Lean
.
Meta
.
isLevelDefEqAuxImpl
:
Level
→
Level
→
MetaM
Bool
Instances For