# Documentation

Lean.Level

def Nat.imax (n : Nat) (m : Nat) :
Equations

Cached hash code, cached results, and other data for Level. hash : 32-bits hasMVar : 1-bit hasParam : 1-bit depth : 24-bits

Equations
Equations
Equations
instance Lean.instBEqData :
Equations
Equations
Equations
Equations
def Lean.Level.mkData (h : UInt64) (depth : ) (hasMVar : ) (hasParam : ) :
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.

Universe level metavariable Id

Instances For
Equations
Equations
@[inline]

Short for LevelMVarId

Equations
Equations
Equations
instance Lean.instForInLMVarIdSetLMVarId {m : Type u_1 → Type u_2} :
Equations
Equations
Equations
instance Lean.instForInLMVarIdMapProdLMVarId {m : Type u_1 → Type u_2} {α : Type} :
ForIn m () ()
Equations
Equations
• Lean.instInhabitedLMVarIdMap = { default := }
inductive Lean.Level :
Instances For
@[implemented_by Lean.Level.data._override]
noncomputable def Lean.Level.data :
Equations
@[export lean_level_hash]
Equations
@[export lean_level_has_mvar]
Equations
@[export lean_level_has_param]
Equations
@[export lean_level_depth]
Equations
Equations
@[export lean_level_mk_zero]
Equations
@[export lean_level_mk_succ]
Equations
@[export lean_level_mk_mvar]
Equations
@[export lean_level_mk_param]
Equations
@[export lean_level_mk_max]
Equations
@[export lean_level_mk_imax]
Equations
Equations
• = match x with | Lean.Level.zero => true | x => false
Equations
• = match x with | => true | x => false
Equations
Equations
Equations
Equations
• = match x with | => true | x => false
Equations
• = match x with | => true | x => false
Equations

If result is true, then forall assignments A which assigns all parameters and metavariables occuring in l, l[A] != zero

Equations
Equations
Equations
Equations
• = match with | Lean.Level.zero => some () | x => none
@[extern lean_level_eq]

occurs u l return true iff u occurs in l.

Equations
Equations
• One or more equations did not get rendered due to their size.

A total order on level expressions that has the following properties

• succ l is an immediate successor of l.
• zero is the minimal element. This total order is used in the normalization procedure.
Equations

Return true if u and v denote the same level. Check is currently incomplete.

Equations
• = ()

Reduce (if possible) universe level by 1

Equations
• leaf:
• num:
• offset:
• maxNode:
• imaxNode:
Instances For
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
Equations
Equations

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.

Equations
• One or more equations did not get rendered due to their size.
@[implemented_by _private.Lean.Level.0.Lean.Level.updateMax!Impl]
Equations
• One or more equations did not get rendered due to their size.
@[implemented_by _private.Lean.Level.0.Lean.Level.updateIMax!Impl]
Equations
• One or more equations did not get rendered due to their size.
@[specialize #[]]
Equations
Equations
• One or more equations did not get rendered due to their size.
• = match s n with | some u' => u' | none =>
Equations
Equations
@[inline]
abbrev Lean.LevelMap (α : Type) :
Equations
@[inline]
Equations
@[inline]
Equations
@[inline]
Equations
@[inline]
Equations
def Lean.Level.find? (u : Lean.Level) (p : ) :
Equations
Equations
• One or more equations did not get rendered due to their size.
• = if p () = true then else
• = if p u = true then pure u else failure
def Lean.Level.any (u : Lean.Level) (p : ) :
Equations
@[inline]
abbrev Nat.toLevel (n : Nat) :
Equations