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

def Lean.Level.Data : Type

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

instance Lean.instInhabitedData : Inhabited Lean.Level.Data

def Lean.Level.Data.hash (c : Lean.Level.Data) : UInt64

instance Lean.instBEqData : BEq Lean.Level.Data

def Lean.Level.Data.depth (c : Lean.Level.Data) : UInt32

def Lean.Level.Data.hasMVar (c : Lean.Level.Data) : Bool

def Lean.Level.Data.hasParam (c : Lean.Level.Data) : Bool

def Lean.Level.mkData (h : UInt64) (depth : optParam Nat 0) (hasMVar : optParam Bool false) (hasParam : optParam Bool false) : Lean.Level.Data

instance Lean.instReprData : Repr Lean.Level.Data

structure Lean.LevelMVarId : Type

• name : Lake.Name

Universe level metavariable Id

instance Lean.instInhabitedLevelMVarId : Inhabited Lean.LevelMVarId

instance Lean.instBEqLevelMVarId : BEq Lean.LevelMVarId

instance Lean.instHashableLevelMVarId : Hashable Lean.LevelMVarId

instance Lean.instReprLevelMVarId : Repr Lean.LevelMVarId

@[inline, reducible]

abbrev Lean.LMVarId : Type

Short for LevelMVarId

instance Lean.instReprLMVarId : Repr Lean.LMVarId

def Lean.LMVarIdSet : Type

instance Lean.instForInLMVarIdSetLMVarId {m : Type u_1 → Type u_2} : ForIn m Lean.LMVarIdSet Lean.LMVarId

def Lean.LMVarIdMap (α : Type) : Type

instance Lean.instEmptyCollectionLMVarIdMap {α : Type} : EmptyCollection (Lean.LMVarIdMap α)

instance Lean.instForInLMVarIdMapProdLMVarId {m : Type u_1 → Type u_2} {α : Type} : ForIn m (Lean.LMVarIdMap α) (Lean.LMVarId × α)

instance Lean.instInhabitedLMVarIdMap {α : Type} : Inhabited (Lean.LMVarIdMap α)

inductive Lean.Level : Type

• zero: Lean.Level
• succ: Lean.Level → Lean.Level
• max: Lean.Level → Lean.Level → Lean.Level
• imax: Lean.Level → Lean.Level → Lean.Level
• param: Lake.Name → Lean.Level
• mvar: Lean.LMVarId → Lean.Level

@[implemented_by Lean.Level.data._override]

noncomputable def Lean.Level.data : Lean.Level → Lean.Level.Data

Equations

• One or more equations did not get rendered due to their size.
• Lean.Level.data Lean.Level.zero = Lean.Level.mkData 2221 0 false
• Lean.Level.data (Lean.Level.mvar mvarId) = Lean.Level.mkData (mixHash 2237 (hash mvarId)) 0 true
• Lean.Level.data (Lean.Level.param name) = Lean.Level.mkData (mixHash 2239 (hash name)) 0 false true

instance Lean.instInhabitedLevel : Inhabited Lean.Level

instance Lean.instReprLevel : Repr Lean.Level

def Lean.Level.hash (u : Lean.Level) : UInt64

instance Lean.Level.instHashableLevel : Hashable Lean.Level

def Lean.Level.depth (u : Lean.Level) : Nat

def Lean.Level.hasMVar (u : Lean.Level) : Bool

def Lean.Level.hasParam (u : Lean.Level) : Bool

@[export lean_level_hash]

def Lean.Level.hashEx (u : Lean.Level) : UInt32

@[export lean_level_has_mvar]

def Lean.Level.hasMVarEx : Lean.Level → Bool

@[export lean_level_has_param]

def Lean.Level.hasParamEx : Lean.Level → Bool

@[export lean_level_depth]

def Lean.Level.depthEx (u : Lean.Level) : UInt32

def Lean.levelZero : Lean.Level

def Lean.mkLevelMVar (mvarId : Lean.LMVarId) : Lean.Level

def Lean.mkLevelParam (name : Lake.Name) : Lean.Level

def Lean.mkLevelSucc (u : Lean.Level) : Lean.Level

def Lean.mkLevelMax (u : Lean.Level) (v : Lean.Level) : Lean.Level

def Lean.mkLevelIMax (u : Lean.Level) (v : Lean.Level) : Lean.Level

def Lean.levelOne : Lean.Level

@[export lean_level_mk_zero]

def Lean.mkLevelZeroEx : Unit → Lean.Level

@[export lean_level_mk_succ]

def Lean.mkLevelSuccEx : Lean.Level → Lean.Level

@[export lean_level_mk_mvar]

def Lean.mkLevelMVarEx : Lean.LMVarId → Lean.Level

@[export lean_level_mk_param]

def Lean.mkLevelParamEx : Lake.Name → Lean.Level

@[export lean_level_mk_max]

def Lean.mkLevelMaxEx : Lean.Level → Lean.Level → Lean.Level

@[export lean_level_mk_imax]

def Lean.mkLevelIMaxEx : Lean.Level → Lean.Level → Lean.Level

def Lean.Level.isZero : Lean.Level → Bool

def Lean.Level.isSucc : Lean.Level → Bool

def Lean.Level.isMax : Lean.Level → Bool

def Lean.Level.isIMax : Lean.Level → Bool

def Lean.Level.isMaxIMax : Lean.Level → Bool

def Lean.Level.isParam : Lean.Level → Bool

def Lean.Level.isMVar : Lean.Level → Bool

def Lean.Level.mvarId! : Lean.Level → Lean.LMVarId

def Lean.Level.isNeverZero : Lean.Level → Bool

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

Equations

• Lean.Level.isNeverZero Lean.Level.zero = false
• Lean.Level.isNeverZero (Lean.Level.param a) = false
• Lean.Level.isNeverZero (Lean.Level.mvar a) = false
• Lean.Level.isNeverZero (Lean.Level.succ a) = true
• Lean.Level.isNeverZero (Lean.Level.max l₁ l₂) = (Lean.Level.isNeverZero l₁ || Lean.Level.isNeverZero l₂)
• Lean.Level.isNeverZero (Lean.Level.imax a l₂) = Lean.Level.isNeverZero l₂

def Lean.Level.ofNat : Nat → Lean.Level

Equations

• Lean.Level.ofNat 0 = Lean.levelZero
• Lean.Level.ofNat (Nat.succ n) = Lean.mkLevelSucc (Lean.Level.ofNat n)

def Lean.Level.addOffsetAux : Nat → Lean.Level → Lean.Level

Equations

• Lean.Level.addOffsetAux 0 x = x
• Lean.Level.addOffsetAux (Nat.succ n) x = Lean.Level.addOffsetAux n (Lean.mkLevelSucc x)

def Lean.Level.addOffset (u : Lean.Level) (n : Nat) : Lean.Level

def Lean.Level.isExplicit : Lean.Level → Bool

def Lean.Level.getOffsetAux : Lean.Level → Nat → Nat

Equations

• Lean.Level.getOffsetAux (Lean.Level.succ u) x = Lean.Level.getOffsetAux u (x + 1)
• Lean.Level.getOffsetAux x x = x

def Lean.Level.getOffset (lvl : Lean.Level) : Nat

def Lean.Level.getLevelOffset : Lean.Level → Lean.Level

Equations

• Lean.Level.getLevelOffset (Lean.Level.succ a) = Lean.Level.getLevelOffset a
• Lean.Level.getLevelOffset x = x

def Lean.Level.toNat (lvl : Lean.Level) : Option Nat

@[extern lean_level_eq]

opaque Lean.Level.beq (a : Lean.Level) (b : Lean.Level) : Bool

instance Lean.Level.instBEqLevel : BEq Lean.Level

def Lean.Level.occurs : Lean.Level → Lean.Level → Bool

occurs u l return true iff u occurs in l.

Equations

• Lean.Level.occurs x (Lean.Level.succ v₁) = (x == Lean.Level.succ v₁ || Lean.Level.occurs x v₁)
• Lean.Level.occurs x (Lean.Level.max v₁ v₂) = (x == Lean.Level.max v₁ v₂ || Lean.Level.occurs x v₁ || Lean.Level.occurs x v₂)
• Lean.Level.occurs x (Lean.Level.imax v₁ v₂) = (x == Lean.Level.imax v₁ v₂ || Lean.Level.occurs x v₁ || Lean.Level.occurs x v₂)
• Lean.Level.occurs x x = (x == x)

def Lean.Level.ctorToNat : Lean.Level → Nat

partial def Lean.Level.normLtAux : Lean.Level → Nat → Lean.Level → Nat → Bool

def Lean.Level.normLt (l₁ : Lean.Level) (l₂ : Lean.Level) : Bool

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.

partial def Lean.Level.normalize (l : Lean.Level) : Lean.Level

def Lean.Level.isEquiv (u : Lean.Level) (v : Lean.Level) : Bool

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

def Lean.Level.dec : Lean.Level → Option Lean.Level

Reduce (if possible) universe level by 1

Equations

• Lean.Level.dec Lean.Level.zero = none
• Lean.Level.dec (Lean.Level.param a) = none
• Lean.Level.dec (Lean.Level.mvar a) = none
• Lean.Level.dec (Lean.Level.succ a) = some a
• Lean.Level.dec (Lean.Level.max l₁ l₂) = do let __do_lift ← Lean.Level.dec l₁ let __do_lift_1 ← Lean.Level.dec l₂ pure (Lean.mkLevelMax __do_lift __do_lift_1)
• Lean.Level.dec (Lean.Level.imax a l₂) = do let __do_lift ← Lean.Level.dec a let __do_lift_1 ← Lean.Level.dec l₂ pure (Lean.mkLevelMax __do_lift __do_lift_1)

inductive Lean.Level.PP.Result : Type

• leaf: Lake.Name → Lean.Level.PP.Result
• num: Nat → Lean.Level.PP.Result
• offset: Lean.Level.PP.Result → Nat → Lean.Level.PP.Result
• maxNode: List Lean.Level.PP.Result → Lean.Level.PP.Result
• imaxNode: List Lean.Level.PP.Result → Lean.Level.PP.Result

def Lean.Level.PP.Result.succ : Lean.Level.PP.Result → Lean.Level.PP.Result

def Lean.Level.PP.Result.max : Lean.Level.PP.Result → Lean.Level.PP.Result → Lean.Level.PP.Result

def Lean.Level.PP.Result.imax : Lean.Level.PP.Result → Lean.Level.PP.Result → Lean.Level.PP.Result

def Lean.Level.PP.toResult : Lean.Level → Lean.Level.PP.Result

Equations

• Lean.Level.PP.toResult Lean.Level.zero = Lean.Level.PP.Result.num 0
• Lean.Level.PP.toResult (Lean.Level.succ a) = Lean.Level.PP.Result.succ (Lean.Level.PP.toResult a)
• Lean.Level.PP.toResult (Lean.Level.max a a_1) = Lean.Level.PP.Result.max (Lean.Level.PP.toResult a) (Lean.Level.PP.toResult a_1)
• Lean.Level.PP.toResult (Lean.Level.imax a a_1) = Lean.Level.PP.Result.imax (Lean.Level.PP.toResult a) (Lean.Level.PP.toResult a_1)
• Lean.Level.PP.toResult (Lean.Level.param a) = Lean.Level.PP.Result.leaf a
• Lean.Level.PP.toResult (Lean.Level.mvar a) = let n := Lean.Name.replacePrefix a.name `_uniq (Lean.Name.mkSimple "?u"); Lean.Level.PP.Result.leaf n

partial def Lean.Level.PP.Result.format : Lean.Level.PP.Result → Bool → Lean.Format

partial def Lean.Level.PP.Result.quote (r : Lean.Level.PP.Result) (prec : Nat) : Lean.Syntax.Level

def Lean.Level.format (u : Lean.Level) : Lean.Format

instance Lean.Level.instToFormatLevel : Lean.ToFormat Lean.Level

instance Lean.Level.instToStringLevel : ToString Lean.Level

def Lean.Level.quote (u : Lean.Level) (prec : optParam Nat 0) : Lean.Syntax.Level

instance Lean.Level.instQuoteLevelMkStr1 : Lean.Quote Lean.Level `level

def Lean.mkLevelMax' (u : Lean.Level) (v : Lean.Level) : Lean.Level

def Lean.simpLevelMax' (u : Lean.Level) (v : Lean.Level) (d : Lean.Level) : Lean.Level

def Lean.mkLevelIMax' (u : Lean.Level) (v : Lean.Level) : Lean.Level

def Lean.simpLevelIMax' (u : Lean.Level) (v : Lean.Level) (d : Lean.Level) : Lean.Level

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]

def Lean.Level.updateSucc! (lvl : Lean.Level) (newLvl : Lean.Level) : Lean.Level

@[implemented_by _private.Lean.Level.0.Lean.Level.updateMax!Impl]

def Lean.Level.updateMax! (lvl : Lean.Level) (newLhs : Lean.Level) (newRhs : Lean.Level) : Lean.Level

@[implemented_by _private.Lean.Level.0.Lean.Level.updateIMax!Impl]

def Lean.Level.updateIMax! (lvl : Lean.Level) (newLhs : Lean.Level) (newRhs : Lean.Level) : Lean.Level

def Lean.Level.mkNaryMax : List Lean.Level → Lean.Level

Equations

• Lean.Level.mkNaryMax [] = Lean.levelZero
• Lean.Level.mkNaryMax [u] = u
• Lean.Level.mkNaryMax (u :: us) = Lean.mkLevelMax' u (Lean.Level.mkNaryMax us)

@[specialize #[]]

def Lean.Level.substParams (u : Lean.Level) (s : Lake.Name → Option Lean.Level) : Lean.Level

def Lean.Level.substParams.go (s : Lake.Name → Option Lean.Level) (u : Lean.Level) : Lean.Level

Equations

• One or more equations did not get rendered due to their size.
• Lean.Level.substParams.go s Lean.Level.zero = Lean.Level.zero
• Lean.Level.substParams.go s (Lean.Level.param n) = match s n with | some u' => u' | none => Lean.Level.param n
• Lean.Level.substParams.go s u = u

def Lean.Level.getParamSubst : List Lake.Name → List Lean.Level → Lake.Name → Option Lean.Level

Equations

• Lean.Level.getParamSubst (p :: ps) (u :: us) x = if (p == x) = true then some u else Lean.Level.getParamSubst ps us x
• Lean.Level.getParamSubst x x x = none

def Lean.Level.instantiateParams (u : Lean.Level) (paramNames : List Lake.Name) (vs : List Lean.Level) : Lean.Level

def Lean.Level.geq (u : Lean.Level) (v : Lean.Level) : Bool

def Lean.Level.geq.go (u : Lean.Level) (v : Lean.Level) : Bool

Equations

• One or more equations did not get rendered due to their size.
• Lean.Level.geq.go u Lean.Level.zero = (u == Lean.Level.zero || true)
• Lean.Level.geq.go u (Lean.Level.max v₁ v₂) = (u == Lean.Level.max v₁ v₂ || Lean.Level.geq.go u v₁ && Lean.Level.geq.go u v₂)
• Lean.Level.geq.go (Lean.Level.max u₁ u₂) v = (Lean.Level.max u₁ u₂ == v || (Lean.Level.geq.go u₁ v || Lean.Level.geq.go u₂ v))
• Lean.Level.geq.go u (Lean.Level.imax v₁ v₂) = (u == Lean.Level.imax v₁ v₂ || Lean.Level.geq.go u v₁ && Lean.Level.geq.go u v₂)
• Lean.Level.geq.go (Lean.Level.imax a u₂) v = (Lean.Level.imax a u₂ == v || Lean.Level.geq.go u₂ v)
• Lean.Level.geq.go (Lean.Level.succ u_2) (Lean.Level.succ v_2) = (Lean.Level.succ u_2 == Lean.Level.succ v_2 || Lean.Level.geq.go u_2 v_2)

@[inline, reducible]

abbrev Lean.LevelMap (α : Type) : Type

@[inline, reducible]

abbrev Lean.PersistentLevelMap (α : Type) : Type

@[inline, reducible]

abbrev Lean.LevelSet : Type

@[inline, reducible]

abbrev Lean.PersistentLevelSet : Type

@[inline, reducible]

abbrev Lean.PLevelSet : Type

def Lean.Level.collectMVars (u : Lean.Level) (s : optParam Lean.LMVarIdSet ∅) : Lean.LMVarIdSet

Equations

• Lean.Level.collectMVars (Lean.Level.succ v) s = Lean.Level.collectMVars v s
• Lean.Level.collectMVars (Lean.Level.max u_2 v) s = Lean.Level.collectMVars u_2 (Lean.Level.collectMVars v s)
• Lean.Level.collectMVars (Lean.Level.imax u_2 v) s = Lean.Level.collectMVars u_2 (Lean.Level.collectMVars v s)
• Lean.Level.collectMVars (Lean.Level.mvar n) s = Lean.RBTree.insert s n
• Lean.Level.collectMVars u s = s

def Lean.Level.find? (u : Lean.Level) (p : Lean.Level → Bool) : Option Lean.Level

def Lean.Level.find?.visit (p : Lean.Level → Bool) (u : Lean.Level) : Option Lean.Level

Equations

• One or more equations did not get rendered due to their size.
• Lean.Level.find?.visit p (Lean.Level.succ v) = if p (Lean.Level.succ v) = true then pure (Lean.Level.succ v) else Lean.Level.find?.visit p v
• Lean.Level.find?.visit p u = if p u = true then pure u else failure

def Lean.Level.any (u : Lean.Level) (p : Lean.Level → Bool) : Bool

@[inline, reducible]

abbrev Nat.toLevel (n : Nat) : Lean.Level