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

Equations

• Nat.imax n m = if m = 0 then 0 else Nat.max n m

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

Equations

• Lean.Level.Data = UInt64

instance Lean.instInhabitedData : Inhabited Lean.Level.Data

Equations

• Lean.instInhabitedData = inferInstanceAs (Inhabited UInt64)

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

Equations

• Lean.Level.Data.hash c = UInt32.toUInt64 (UInt64.toUInt32 c)

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

• Lean.Level.Data.depth c = UInt64.toUInt32 (UInt64.shiftRight c 40)

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

Equations

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

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

Equations

• Lean.Level.Data.hasParam c = (UInt64.land (UInt64.shiftRight c 33) 1 == 1)

def Lean.Level.mkData (h : UInt64) (depth : optParam Nat 0) (hasMVar : optParam Bool false) (hasParam : optParam 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 : Lake.Name

instance Lean.instInhabitedLevelMVarId : Inhabited Lean.LevelMVarId

Equations

• Lean.instInhabitedLevelMVarId = { default := { name := default } }

instance Lean.instBEqLevelMVarId : BEq Lean.LevelMVarId

Equations

• Lean.instBEqLevelMVarId = { beq := Lean.beqLevelMVarId✝ }

instance Lean.instHashableLevelMVarId : Hashable Lean.LevelMVarId

Equations

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

instance Lean.instReprLevelMVarId : Repr Lean.LevelMVarId

Equations

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

@[inline, reducible]

abbrev Lean.LMVarId : Type

Short for LevelMVarId

Equations

• Lean.LMVarId = Lean.LevelMVarId

instance Lean.instReprLMVarId : Repr Lean.LMVarId

Equations

• Lean.instReprLMVarId = { reprPrec := fun (n : Lean.LMVarId) (p : Nat) => reprPrec n.name p }

def Lean.LMVarIdSet : Type

Equations

• Lean.LMVarIdSet = Lean.RBTree Lean.LMVarId fun (x x_1 : Lean.LMVarId) => Lean.Name.quickCmp x.name x_1.name

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

Equations

• Lean.instForInLMVarIdSetLMVarId = inferInstanceAs (ForIn m (Lean.RBTree Lean.LMVarId fun (x x_1 : Lean.LMVarId) => Lean.Name.quickCmp x.name x_1.name) Lean.LMVarId)

def Lean.LMVarIdMap (α : Type) : Type

Equations

• Lean.LMVarIdMap α = Lean.RBMap Lean.LMVarId α fun (x x_1 : Lean.LMVarId) => Lean.Name.quickCmp x.name x_1.name

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

Equations

• Lean.instEmptyCollectionLMVarIdMap = inferInstanceAs (EmptyCollection (Lean.RBMap Lean.LMVarId α fun (x x_1 : Lean.LMVarId) => Lean.Name.quickCmp x.name x_1.name))

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 (x x_1 : Lean.LMVarId) => Lean.Name.quickCmp x.name x_1.name) (Lean.LMVarId × α))

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

Equations

• Lean.instInhabitedLMVarIdMap = { default := ∅ }

@[implemented_by Lean.Level.data._override]

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

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

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

Equations

• Lean.Level.hash u = Lean.Level.Data.hash (Lean.Level.data u)

instance Lean.Level.instHashableLevel : Hashable Lean.Level

Equations

• Lean.Level.instHashableLevel = { hash := Lean.Level.hash }

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

Equations

• Lean.Level.depth u = UInt32.toNat (Lean.Level.Data.depth (Lean.Level.data u))

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

Equations

• Lean.Level.hasMVar u = Lean.Level.Data.hasMVar (Lean.Level.data u)

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

Equations

• Lean.Level.hasParam u = Lean.Level.Data.hasParam (Lean.Level.data u)

@[export lean_level_hash]

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

Equations

• Lean.Level.hashEx u = UInt64.toUInt32 (hash u)

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

Equations

• Lean.Level.depthEx u = Lean.Level.Data.depth (Lean.Level.data u)

def Lean.levelZero : Lean.Level

Equations

• Lean.levelZero = Lean.Level.zero

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

Equations

• Lean.mkLevelMVar mvarId = Lean.Level.mvar mvarId

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

Equations

• Lean.mkLevelParam name = Lean.Level.param name

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

Equations

• Lean.mkLevelSucc u = Lean.Level.succ u

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

Equations

• Lean.mkLevelMax u v = Lean.Level.max u v

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

Equations

• Lean.mkLevelIMax u v = Lean.Level.imax u v

def Lean.levelOne : Lean.Level

Equations

• Lean.levelOne = Lean.mkLevelSucc Lean.levelZero

@[export lean_level_mk_zero]

def Lean.mkLevelZeroEx : Unit → Lean.Level

Equations

• Lean.mkLevelZeroEx x = Lean.levelZero

@[export lean_level_mk_succ]

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

Equations

• Lean.mkLevelSuccEx = Lean.mkLevelSucc

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

Equations

• Lean.mkLevelParamEx = Lean.mkLevelParam

@[export lean_level_mk_max]

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

Equations

• Lean.mkLevelMaxEx = Lean.mkLevelMax

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

Equations

• Lean.Level.isZero x = match x with | Lean.Level.zero => true | x => false

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

Equations

• Lean.Level.isSucc x = match x with | Lean.Level.succ a => true | x => false

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

Equations

• Lean.Level.isMax x = match x with | Lean.Level.max a a_1 => true | x => false

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

Equations

• Lean.Level.isIMax x = match x with | Lean.Level.imax a a_1 => true | x => false

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

Equations

• Lean.Level.isMaxIMax x = match x with | Lean.Level.max a a_1 => true | Lean.Level.imax a a_1 => true | x => false

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

Equations

• Lean.Level.isParam x = match x with | Lean.Level.param a => true | x => false

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

Equations

• Lean.Level.isMVar x = match x with | Lean.Level.mvar a => true | x => false

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

Equations

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

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

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)

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 (Nat.succ n) x = Lean.Level.addOffsetAux n (Lean.mkLevelSucc x)

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

Equations

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

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

Equations

• Lean.Level.getOffset lvl = Lean.Level.getOffsetAux lvl 0

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

Equations

• Lean.Level.toNat lvl = match Lean.Level.getLevelOffset lvl with | Lean.Level.zero => some (Lean.Level.getOffset lvl) | x => none

@[extern lean_level_eq]

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

instance Lean.Level.instBEqLevel : BEq Lean.Level

Equations

• Lean.Level.instBEqLevel = { beq := Lean.Level.beq }

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

Equations

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

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.

Equations

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

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.

Equations

• Lean.Level.isEquiv u v = (u == v || Lean.Level.normalize u == Lean.Level.normalize v)

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

Equations

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

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

Equations

• Lean.Level.PP.Result.max x✝ x = match x✝, x with | f, Lean.Level.PP.Result.maxNode Fs => Lean.Level.PP.Result.maxNode (f :: Fs) | f₁, f₂ => Lean.Level.PP.Result.maxNode [f₁, f₂]

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

Equations

• Lean.Level.PP.Result.imax x✝ x = match x✝, x with | f, Lean.Level.PP.Result.imaxNode Fs => Lean.Level.PP.Result.imaxNode (f :: Fs) | f₁, f₂ => Lean.Level.PP.Result.imaxNode [f₁, f₂]

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

Equations

• Lean.Level.format u = Lean.Level.PP.Result.format (Lean.Level.PP.toResult u) true

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

Equations

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

instance Lean.Level.instToStringLevel : ToString Lean.Level

Equations

• Lean.Level.instToStringLevel = { toString := fun (u : Lean.Level) => Lean.Format.pretty (Lean.Level.format u) }

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

Equations

• Lean.Level.quote u prec = Lean.Level.PP.Result.quote (Lean.Level.PP.toResult u) prec

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

Equations

• Lean.Level.instQuoteLevelMkStr1 = Lean.Quote.mk `level fun (u : Lean.Level) => Lean.Level.quote u

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

Equations

• Lean.mkLevelMax' u v = Lean.mkLevelMaxCore u v fun (x : Unit) => Lean.mkLevelMax u v

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

Equations

• Lean.simpLevelMax' u v d = Lean.mkLevelMaxCore u v fun (x : Unit) => d

def Lean.mkLevelIMax' (u : Lean.Level) (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 : Lean.Level) (v : Lean.Level) (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 : Lean.Level) (newLvl : Lean.Level) : Lean.Level

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Lean.Level.substParams u s = Lean.Level.substParams.go s u

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

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

Equations

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

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

Equations

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

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

Equations

• Lean.LevelMap α = Lean.HashMap Lean.Level α

@[inline, reducible]

abbrev Lean.PersistentLevelMap (α : Type) : Type

Equations

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

@[inline, reducible]

abbrev Lean.LevelSet : Type

Equations

• Lean.LevelSet = Lean.HashSet Lean.Level

@[inline, reducible]

abbrev Lean.PersistentLevelSet : Type

Equations

• Lean.PersistentLevelSet = Lean.PHashSet Lean.Level

@[inline, reducible]

abbrev Lean.PLevelSet : Type

Equations

• Lean.PLevelSet = Lean.PersistentLevelSet

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

Equations

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

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

Equations

• Lean.Level.any u p = Option.isSome (Lean.Level.find? u p)

@[inline, reducible]

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

Equations

• Nat.toLevel n = Lean.Level.ofNat n