def Nat.imax (n 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

Equations

• Lean.instInhabitedData = inferInstanceAs (Inhabited UInt64)

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

instance Lean.instBEqData : BEq Lean.Level.Data

Equations

• Lean.instBEqData = { beq := fun (a b : UInt64) => a == b }

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

Equations

• c.depth = (UInt64.shiftRight c 40).toUInt32

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

Equations

• c.hasMVar = ((UInt64.shiftRight c 32).land 1 == 1)

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

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

Equations

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

instance Lean.instReprData : Repr Lean.Level.Data

Equations

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

structure Lean.LevelMVarId : Type

Universe level metavariable Id

• name : Lean.Name

instance Lean.instInhabitedLevelMVarId : Inhabited Lean.LevelMVarId

instance Lean.instBEqLevelMVarId : BEq Lean.LevelMVarId

instance Lean.instHashableLevelMVarId : Hashable Lean.LevelMVarId

Equations

• Lean.instHashableLevelMVarId = { hash := Lean.hashLevelMVarId✝ }

instance Lean.instReprLevelMVarId : Repr Lean.LevelMVarId

Equations

• Lean.instReprLevelMVarId = { reprPrec := Lean.reprLevelMVarId✝ }

@[reducible, inline]

abbrev Lean.LMVarId : Type

Short for LevelMVarId

Equations

• Lean.LMVarId = Lean.LevelMVarId

instance Lean.instReprLMVarId : Repr Lean.LMVarId

def Lean.LMVarIdSet : Type

Equations

• Lean.LMVarIdSet = Lean.RBTree Lean.LMVarId fun (x1 x2 : Lean.LMVarId) => x1.name.quickCmp x2.name

instance Lean.instLMVarIdSetInhabited : Inhabited Lean.LMVarIdSet

instance Lean.instLMVarIdSetEmptyCollection : EmptyCollection Lean.LMVarIdSet

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 × α)

Equations

• Lean.instForInLMVarIdMapProdLMVarId = inferInstanceAs (ForIn m (Lean.RBMap Lean.LMVarId α fun (x1 x2 : Lean.LMVarId) => x1.name.quickCmp x2.name) (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: Lean.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.zero.data = Lean.Level.mkData 2221
• (Lean.Level.mvar mvarId).data = Lean.Level.mkData (mixHash 2237 (hash mvarId)) 0 true
• (Lean.Level.param name).data = Lean.Level.mkData (mixHash 2239 (hash name)) 0 false true
• u.succ.data = Lean.Level.mkData (mixHash 2243 u.data.hash) (u.data.depth.toNat + 1) u.data.hasMVar u.data.hasParam

instance Lean.instInhabitedLevel : Inhabited Lean.Level

Equations

• Lean.instInhabitedLevel = { default := Lean.Level.zero }

instance Lean.instReprLevel : Repr Lean.Level

Equations

• Lean.instReprLevel = { reprPrec := Lean.reprLevel✝ }

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

instance Lean.Level.instHashable : 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

Equations

• Lean.Level.hasMVarEx = Lean.Level.hasMVar

@[export lean_level_has_param]

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

Equations

• Lean.Level.hasParamEx = Lean.Level.hasParam

@[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 : Lean.Name) : Lean.Level

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

Equations

• Lean.mkLevelSucc u = u.succ

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

Equations

• Lean.mkLevelMax u v = u.max v

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

def Lean.levelOne : Lean.Level

Equations

• Lean.levelOne = Lean.mkLevelSucc Lean.levelZero

@[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

Equations

• Lean.mkLevelMVarEx = Lean.mkLevelMVar

@[export lean_level_mk_param]

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

Equations

• Lean.mkLevelParamEx = Lean.mkLevelParam

@[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

Equations

• Lean.mkLevelIMaxEx = Lean.mkLevelIMax

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

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

Equations

• a.succ.isSucc = true
• x.isSucc = false

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

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

Equations

• (a.imax a_1).isIMax = true
• x.isIMax = false

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

Equations

• (a.max a_1).isMaxIMax = true
• (a.imax a_1).isMaxIMax = true
• x.isMaxIMax = false

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

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

Equations

• (Lean.Level.mvar a).isMVar = true
• x.isMVar = false

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 occurring in l, l[A] != zero

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

instance Lean.Level.instOfNat (n : Nat) : OfNat Lean.Level n

Equations

• Lean.Level.instOfNat n = { ofNat := Lean.Level.ofNat n }

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

Equations

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

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

Equations

• u.addOffset n = Lean.Level.addOffsetAux n u

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

Equations

• Lean.Level.zero.isExplicit = true
• u.succ.isExplicit = (!u.hasMVar && !u.hasParam && u.isExplicit)
• x.isExplicit = false

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

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

Equations

• lvl.getOffset = lvl.getOffsetAux 0

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

Equations

• a.succ.getLevelOffset = a.getLevelOffset
• x.getLevelOffset = x

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

@[extern lean_level_eq]

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

instance Lean.Level.instBEq : BEq Lean.Level

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

occurs u l return true iff u occurs in l.

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

@[irreducible]

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

def Lean.Level.normLt (l₁ 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.

Equations

• l₁.normLt l₂ = l₁.normLtAux 0 l₂ 0

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

def Lean.Level.isEquiv (u 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

inductive Lean.Level.PP.Result : Type

• leaf: Lean.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

Equations

• (f.offset k).succ = f.offset (k + 1)
• (Lean.Level.PP.Result.num k).succ = Lean.Level.PP.Result.num (k + 1)
• x.succ = x.offset 1

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 (l : Lean.Level) (mvars : Bool) : Lean.Level.PP.Result

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) (mvars : Bool) : Lean.Format

instance Lean.Level.instToFormat : Lean.ToFormat Lean.Level

Equations

• Lean.Level.instToFormat = { format := fun (u : Lean.Level) => u.format true }

instance Lean.Level.instToString : ToString Lean.Level

def Lean.Level.quote (u : Lean.Level) (prec : Nat := 0) (mvars : Bool := true) : Lean.Syntax.Level

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

Equations

• Lean.Level.instQuoteMkStr1 = { quote := fun (u : Lean.Level) => u.quote }

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

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

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

Equations

• Lean.mkLevelIMax' u v = Lean.mkLevelIMaxCore✝ u v fun (x : Unit) => Lean.mkLevelIMax u v

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

Equations

• Lean.simpLevelIMax' u v d = Lean.mkLevelIMaxCore✝ u v fun (x : Unit) => d

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 newLvl : Lean.Level) : Lean.Level

Equations

• a.succ.updateSucc! newLvl = Lean.mkLevelSucc newLvl
• lvl.updateSucc! newLvl = panicWithPosWithDecl "Lean.Level" "Lean.Level.updateSucc!" 547 14 "succ level expected"

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

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

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

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

Equations

• (a.imax a_1).updateIMax! newLhs newRhs = Lean.mkLevelIMax' newLhs newRhs
• lvl.updateIMax! newLhs newRhs = panicWithPosWithDecl "Lean.Level" "Lean.Level.updateIMax!" 569 16 "imax level expected"

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 : Lean.Name → Option Lean.Level) : Lean.Level

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

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

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

Equations

• u.instantiateParams paramNames vs = u.substParams (Lean.Level.getParamSubst paramNames vs)

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

Equations

• u.geq v = Lean.Level.geq.go u.normalize v.normalize

@[irreducible]

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

@[reducible, inline]

abbrev Lean.LevelMap (α : Type) : Type

@[reducible, inline]

abbrev Lean.PersistentLevelMap (α : Type) : Type

Equations

• Lean.PersistentLevelMap α = Lean.PHashMap Lean.Level α

@[reducible, inline]

abbrev Lean.LevelSet : Type

@[reducible, inline]

abbrev Lean.PersistentLevelSet : Type

Equations

• Lean.PersistentLevelSet = Lean.PHashSet Lean.Level

@[reducible, inline]

abbrev Lean.PLevelSet : Type

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

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

Equations

• u.find? p = Lean.Level.find?.visit p u

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

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

@[reducible, inline]

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