Cached hash code, cached results, and other data for Level
.
hash : 32-bits
hasMVar : 1-bit
hasParam : 1-bit
depth : 24-bits
Equations
Instances For
Equations
Equations
instance
Lean.instForInLMVarIdMapProdLMVarId
{m : Type u_1 → Type u_2}
{α : Type}
:
ForIn m (LMVarIdMap α) (LMVarId × α)
Equations
@[implemented_by Lean.Level.data._override]
Equations
Instances For
@[export lean_level_mk_max]
Equations
Instances For
@[export lean_level_mk_imax]
Equations
Instances For
If result is true, then forall assignments A
which assigns all parameters and metavariables occurring
in l
, l[A] != zero
Equations
Instances For
Return true if u
and v
denote the same level.
Check is currently incomplete.
Equations
Instances For
Reduce (if possible) universe level by 1
Equations
Instances For
Equations
Instances For
The update functions try to avoid allocating new values using pointer equality.
Note that if the update*!
functions are used under a match-expression,
the compiler will eliminate the double-match.
@[implemented_by _private.Lean.Level.0.Lean.Level.updateSucc!Impl]
Equations
Instances For
@[implemented_by _private.Lean.Level.0.Lean.Level.updateMax!Impl]
Equations
Instances For
@[implemented_by _private.Lean.Level.0.Lean.Level.updateIMax!Impl]