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

Equations

• n.imax m = if m = 0 then 0 else n.max 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

Instances For

• Lean.instBEqData
• Lean.instInhabitedData
• Lean.instReprData

instance Lean.instInhabitedData : Inhabited Lean.Level.Data

Equations

• Lean.instInhabitedData = inferInstanceAs (Inhabited UInt64)

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

Equations

• c.hash = (UInt64.toUInt32 c).toUInt64

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

Equations

• c.hasParam = ((UInt64.shiftRight c 33).land 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

Instances For

• Lean.Meta.instReduceEvalLevelMVarId_qq
• Lean.instBEqLevelMVarId
• Lean.instHashableLevelMVarId
• Lean.instInhabitedLevelMVarId
• Lean.instReprLevelMVarId
• Mathlib.instToExprLevelMVarId_mathlib
• instToExprLevelMVarId_qq

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✝ }

@[reducible, inline]

abbrev Lean.LMVarId : Type

Short for LevelMVarId

Equations

• Lean.LMVarId = Lean.LevelMVarId

Instances For

• Lean.instForInLMVarIdSetLMVarId
• Lean.instReprLMVarId

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) => x.name.quickCmp x_1.name

Instances For

• Lean.instForInLMVarIdSetLMVarId

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) => x.name.quickCmp x_1.name) Lean.LMVarId)

def Lean.LMVarIdMap (α : Type) : Type

Equations

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

Instances For

• Lean.instEmptyCollectionLMVarIdMap
• Lean.instForInLMVarIdMapProdLMVarId
• Lean.instInhabitedLMVarIdMap

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

Equations

• Lean.instEmptyCollectionLMVarIdMap = inferInstanceAs (EmptyCollection (Lean.RBMap Lean.LMVarId α fun (x x_1 : Lean.LMVarId) => x.name.quickCmp 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) => x.name.quickCmp x_1.name) (Lean.LMVarId × α))

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

Equations

• Lean.instInhabitedLMVarIdMap = { default := ∅ }

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

Instances For

• Lean.Level.instBEq
• Lean.Level.instHashable
• Lean.Level.instOfNat
• Lean.Level.instQuoteMkStr1
• Lean.Level.instToFormat
• Lean.Level.instToString
• Lean.MessageData.instCoeLevel
• Lean.instInhabitedLevel
• Lean.instReprLevel
• Lean.instToMessageDataLevel
• Mathlib.instToExprLevel_mathlib
• instToExprLevel_qq

@[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 0 false
• (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

Equations

• u.hash = u.data.hash

instance Lean.Level.instHashable : Hashable Lean.Level

Equations

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

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

Equations

• u.depth = u.data.depth.toNat

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

Equations

• u.hasMVar = u.data.hasMVar

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

Equations

• u.hasParam = u.data.hasParam

@[export lean_level_hash]

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

Equations

• u.hashEx = (hash u).toUInt32

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

• u.depthEx = u.data.depth

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 = u.succ

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

Equations

• Lean.mkLevelMax u v = u.max v

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

Equations

• Lean.mkLevelIMax u v = u.imax 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

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• x.mvarId! = match x with | Lean.Level.mvar mvarId => mvarId | x => panicWithPosWithDecl "Lean.Level" "Lean.Level.mvarId!" 194 19 "metavariable expected"

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.zero.isNeverZero = false
• (Lean.Level.param a).isNeverZero = false
• (Lean.Level.mvar a).isNeverZero = false
• a.succ.isNeverZero = true
• (l₁.max l₂).isNeverZero = (l₁.isNeverZero || l₂.isNeverZero)
• (a.imax l₂).isNeverZero = l₂.isNeverZero

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

Equations

• Lean.Level.ofNat 0 = Lean.levelZero
• Lean.Level.ofNat n.succ = 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 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

Equations

• u.succ.getOffsetAux x = u.getOffsetAux (x + 1)
• x✝.getOffsetAux x = x

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

Equations

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

@[extern lean_level_eq]

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

instance Lean.Level.instBEq : BEq Lean.Level

Equations

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

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

occurs u l return true iff u occurs in l.

Equations

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

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

Equations

• x.ctorToNat = match x with | Lean.Level.zero => 0 | Lean.Level.param a => 1 | Lean.Level.mvar a => 2 | a.succ => 3 | a.max a_1 => 4 | a.imax a_1 => 5

@[irreducible]

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

• l₁.normLt l₂ = l₁.normLtAux 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

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

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

Reduce (if possible) universe level by 1

Equations

• Lean.Level.zero.dec = none
• (Lean.Level.param a).dec = none
• (Lean.Level.mvar a).dec = none
• a.succ.dec = some a
• (l₁.max l₂).dec = do let __do_lift ← l₁.dec let __do_lift_1 ← l₂.dec pure (Lean.mkLevelMax __do_lift __do_lift_1)
• (a.imax l₂).dec = do let __do_lift ← a.dec let __do_lift_1 ← l₂.dec 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

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

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

Equations

• x✝.max 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

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

Equations

• Lean.Level.PP.toResult Lean.Level.zero mvars = Lean.Level.PP.Result.num 0
• Lean.Level.PP.toResult a.succ mvars = (Lean.Level.PP.toResult a mvars).succ
• Lean.Level.PP.toResult (a.max a_1) mvars = (Lean.Level.PP.toResult a mvars).max (Lean.Level.PP.toResult a_1 mvars)
• Lean.Level.PP.toResult (a.imax a_1) mvars = (Lean.Level.PP.toResult a mvars).imax (Lean.Level.PP.toResult a_1 mvars)
• Lean.Level.PP.toResult (Lean.Level.param a) mvars = Lean.Level.PP.Result.leaf a
• Lean.Level.PP.toResult (Lean.Level.mvar a) mvars = if mvars = true then Lean.Level.PP.Result.leaf (a.name.replacePrefix `_uniq (Lean.Name.mkSimple "?u")) else Lean.Level.PP.Result.leaf `_

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

Equations

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

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

Equations

• Lean.Level.instToString = { toString := fun (u : Lean.Level) => (Std.format u).pretty Std.Format.defWidth 0 }

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

Equations

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

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

Equations

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

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

• lvl.updateSucc! newLvl = match lvl with | a.succ => Lean.mkLevelSucc newLvl | x => 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 : Lean.Level) (newLhs : Lean.Level) (newRhs : Lean.Level) : Lean.Level

Equations

• lvl.updateMax! newLhs newRhs = match lvl with | a.max a_1 => Lean.mkLevelMax' newLhs newRhs | x => panicWithPosWithDecl "Lean.Level" "Lean.Level.updateMax!" 558 15 "max level expected"

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

• lvl.updateIMax! newLhs newRhs = match lvl with | a.imax a_1 => Lean.mkLevelIMax' newLhs newRhs | x => 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 : Lake.Name → Option Lean.Level) : Lean.Level

Equations

• u.substParams 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

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

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

Equations

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

@[irreducible]

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

Equations

• Lean.Level.geq.go u Lean.Level.zero = (u == Lean.Level.zero || true)
• Lean.Level.geq.go u (v₁.max v₂) = (u == v₁.max v₂ || Lean.Level.geq.go u v₁ && Lean.Level.geq.go u v₂)
• Lean.Level.geq.go (u₁.max u₂) v = (u₁.max u₂ == v || (Lean.Level.geq.go u₁ v || Lean.Level.geq.go u₂ v))
• Lean.Level.geq.go u (v₁.imax v₂) = (u == v₁.imax v₂ || Lean.Level.geq.go u v₁ && Lean.Level.geq.go u v₂)
• Lean.Level.geq.go (a.imax u₂) v = (a.imax u₂ == v || Lean.Level.geq.go u₂ v)
• Lean.Level.geq.go u_2.succ v_2.succ = (u_2.succ == v_2.succ || Lean.Level.geq.go u_2 v_2)
• Lean.Level.geq.go u v = (u == v || let v' := v.getLevelOffset; (u.getLevelOffset == v' || v'.isZero) && decide (u.getOffset ≥ v.getOffset))

@[reducible, inline]

abbrev Lean.LevelMap (α : Type) : Type

Equations

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

@[reducible, inline]

abbrev Lean.PersistentLevelMap (α : Type) : Type

Equations

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

@[reducible, inline]

abbrev Lean.LevelSet : Type

Equations

• Lean.LevelSet = Lean.HashSet Lean.Level

@[reducible, inline]

abbrev Lean.PersistentLevelSet : Type

Equations

• Lean.PersistentLevelSet = Lean.PHashSet Lean.Level

@[reducible, inline]

abbrev Lean.PLevelSet : Type

Equations

• Lean.PLevelSet = Lean.PersistentLevelSet

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

Equations

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

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

Equations

• Lean.Level.find?.visit p v.succ = if p v.succ = true then pure v.succ else Lean.Level.find?.visit p v
• Lean.Level.find?.visit p (u_2.max v) = if p (u_2.max v) = true then pure (u_2.max v) else HOrElse.hOrElse (Lean.Level.find?.visit p u_2) fun (x : Unit) => Lean.Level.find?.visit p v
• Lean.Level.find?.visit p (u_2.imax v) = if p (u_2.imax v) = true then pure (u_2.imax v) else HOrElse.hOrElse (Lean.Level.find?.visit p u_2) fun (x : Unit) => 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

• u.any p = (u.find? p).isSome

@[reducible, inline]

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

Equations

• n.toLevel = Lean.Level.ofNat n