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

Equations

• Lean.instInhabitedData = inferInstanceAs (Inhabited UInt64)

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

Equations

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

instance Lean.instBEqData : BEq Level.Data

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

instance Lean.instReprData : Repr Level.Data

Equations

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

structure Lean.LevelMVarId : Type

Universe level metavariable Id

• name : Name

Instances For

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

instance Lean.instInhabitedLevelMVarId : Inhabited LevelMVarId

Equations

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

instance Lean.instBEqLevelMVarId : BEq LevelMVarId

Equations

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

instance Lean.instHashableLevelMVarId : Hashable LevelMVarId

Equations

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

instance Lean.instReprLevelMVarId : Repr 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 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 (x1 x2 : Lean.LMVarId) => x1.name.quickCmp x2.name

Instances For

• Lean.instForInLMVarIdSetLMVarId
• Lean.instLMVarIdSetEmptyCollection
• Lean.instLMVarIdSetInhabited

instance Lean.instLMVarIdSetInhabited : Inhabited LMVarIdSet

Equations

• Lean.instLMVarIdSetInhabited = Lean.instInhabitedRBTree

instance Lean.instLMVarIdSetEmptyCollection : EmptyCollection LMVarIdSet

Equations

• Lean.instLMVarIdSetEmptyCollection = Lean.instEmptyCollectionRBTree Lean.LMVarId fun (x1 x2 : Lean.LMVarId) => x1.name.quickCmp x2.name

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

Equations

• Lean.instForInLMVarIdSetLMVarId = inferInstanceAs (ForIn m (Lean.RBTree Lean.LMVarId fun (x1 x2 : Lean.LMVarId) => x1.name.quickCmp x2.name) Lean.LMVarId)

def Lean.LMVarIdMap (α : Type) : Type

Equations

• Lean.LMVarIdMap α = Lean.RBMap Lean.LMVarId α fun (x1 x2 : Lean.LMVarId) => x1.name.quickCmp x2.name

Instances For

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

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

Equations

• Lean.instEmptyCollectionLMVarIdMap = inferInstanceAs (EmptyCollection (Lean.RBMap Lean.LMVarId α fun (x1 x2 : Lean.LMVarId) => x1.name.quickCmp x2.name))

instance Lean.instForInLMVarIdMapProdLMVarId {m : Type u_1 → Type u_2} {α : Type} : ForIn m (LMVarIdMap α) (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 (LMVarIdMap α)

Equations

• Lean.instInhabitedLMVarIdMap = { default := ∅ }

@[implemented_by Lean.Level.data._override]

noncomputable def Lean.Level.data : 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

inductive Lean.Level : Type

• zero : Level
• succ : Level → Level
• max : Level → Level → Level
• imax : Level → Level → Level
• param : Name → Level
• mvar : LMVarId → 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

instance Lean.instInhabitedLevel : Inhabited Level

Equations

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

instance Lean.instReprLevel : Repr Level

Equations

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

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

Equations

• u.hash = u.data.hash

instance Lean.Level.instHashable : Hashable Level

Equations

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

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

Equations

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

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

Equations

• u.hasMVar = u.data.hasMVar

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

Equations

• u.hasParam = u.data.hasParam

@[export lean_level_hash]

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

Equations

• u.hashEx = (hash u).toUInt32

@[export lean_level_has_mvar]

def Lean.Level.hasMVarEx : Level → Bool

Equations

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

@[export lean_level_has_param]

def Lean.Level.hasParamEx : Level → Bool

Equations

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

@[export lean_level_depth]

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

Equations

• u.depthEx = u.data.depth

def Lean.levelZero : Level

Equations

• Lean.levelZero = Lean.Level.zero

def Lean.mkLevelMVar (mvarId : LMVarId) : Level

Equations

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

def Lean.mkLevelParam (name : Name) : Level

Equations

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

def Lean.mkLevelSucc (u : Level) : Level

Equations

• Lean.mkLevelSucc u = u.succ

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

Equations

• Lean.mkLevelMax u v = u.max v

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

Equations

• Lean.mkLevelIMax u v = u.imax v

def Lean.levelOne : Level

Equations

• Lean.levelOne = Lean.mkLevelSucc Lean.levelZero

@[export lean_level_mk_zero]

def Lean.mkLevelZeroEx : Unit → Level

Equations

• Lean.mkLevelZeroEx x✝ = Lean.levelZero

@[export lean_level_mk_succ]

def Lean.mkLevelSuccEx : Level → Level

Equations

• Lean.mkLevelSuccEx = Lean.mkLevelSucc

@[export lean_level_mk_mvar]

def Lean.mkLevelMVarEx : LMVarId → Level

Equations

• Lean.mkLevelMVarEx = Lean.mkLevelMVar

@[export lean_level_mk_param]

def Lean.mkLevelParamEx : Name → Level

Equations

• Lean.mkLevelParamEx = Lean.mkLevelParam

@[export lean_level_mk_max]

def Lean.mkLevelMaxEx : Level → Level → Level

Equations

• Lean.mkLevelMaxEx = Lean.mkLevelMax

@[export lean_level_mk_imax]

def Lean.mkLevelIMaxEx : Level → Level → Level

Equations

• Lean.mkLevelIMaxEx = Lean.mkLevelIMax

def Lean.Level.isZero : Level → Bool

Equations

• Lean.Level.zero.isZero = true
• x✝.isZero = false

def Lean.Level.isSucc : Level → Bool

Equations

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

def Lean.Level.isMax : Level → Bool

Equations

• (a.max a_1).isMax = true
• x✝.isMax = false

def Lean.Level.isIMax : Level → Bool

Equations

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

def Lean.Level.isMaxIMax : Level → Bool

Equations

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

def Lean.Level.isParam : Level → Bool

Equations

• (Lean.Level.param a).isParam = true
• x✝.isParam = false

def Lean.Level.isMVar : Level → Bool

Equations

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

def Lean.Level.mvarId! : Level → LMVarId

Equations

• (Lean.Level.mvar a).mvarId! = a
• x✝.mvarId! = panicWithPosWithDecl "Lean.Level" "Lean.Level.mvarId!" 194 19 "metavariable expected"

def Lean.Level.isNeverZero : 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 → 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 Level n

Equations

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

def Lean.Level.addOffsetAux : Nat → Level → 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 : Level) (n : Nat) : Level

Equations

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

def Lean.Level.isExplicit : Level → Bool

Equations

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

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

Equations

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

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

Equations

• lvl.getOffset = lvl.getOffsetAux 0

def Lean.Level.getLevelOffset : Level → Level

Equations

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

def Lean.Level.toNat (lvl : 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 b : Level) : Bool

instance Lean.Level.instBEq : BEq Level

Equations

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

def Lean.Level.occurs : Level → 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 : Level → Nat

Equations

• Lean.Level.zero.ctorToNat = 0
• (Lean.Level.param a).ctorToNat = 1
• (Lean.Level.mvar a).ctorToNat = 2
• a.succ.ctorToNat = 3
• (l₁.max l₂).ctorToNat = 4
• (a.imax l₂).ctorToNat = 5

@[irreducible]

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

Equations

• l₁.succ.normLtAux x✝² x✝¹ x✝ = l₁.normLtAux (x✝² + 1) x✝¹ x✝
• x✝².normLtAux x✝¹ l₂.succ x✝ = x✝².normLtAux x✝¹ l₂ (x✝ + 1)
• (l₁₁.max l₁₂).normLtAux x✝¹ (l₂₁.max l₂₂) x✝ = if (l₁₁.max l₁₂ == l₂₁.max l₂₂) = true then decide (x✝¹ < x✝) else if (l₁₁ != l₂₁) = true then l₁₁.normLtAux 0 l₂₁ 0 else l₁₂.normLtAux 0 l₂₂ 0
• (l₁₁.imax l₁₂).normLtAux x✝¹ (l₂₁.imax l₂₂) x✝ = if (l₁₁.imax l₁₂ == l₂₁.imax l₂₂) = true then decide (x✝¹ < x✝) else if (l₁₁ != l₂₁) = true then l₁₁.normLtAux 0 l₂₁ 0 else l₁₂.normLtAux 0 l₂₂ 0
• (Lean.Level.param n₁).normLtAux x✝¹ (Lean.Level.param n₂) x✝ = if (n₁ == n₂) = true then decide (x✝¹ < x✝) else n₁.lt n₂
• (Lean.Level.mvar n₁).normLtAux x✝¹ (Lean.Level.mvar n₂) x✝ = if (n₁ == n₂) = true then decide (x✝¹ < x✝) else n₁.name.lt n₂.name
• x✝³.normLtAux x✝² x✝¹ x✝ = if (x✝³ == x✝¹) = true then decide (x✝² < x✝) else decide (x✝³.ctorToNat < x✝¹.ctorToNat)

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

def Lean.Level.isEquiv (u v : 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 : Level → Option 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 : Name → Result
• num : Nat → Result
• offset : Result → Nat → Result
• maxNode : List Result → Result
• imaxNode : List Result → Result

def Lean.Level.PP.Result.succ : Result → 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 : Result → Result → Result

Equations

• x✝.max (Lean.Level.PP.Result.maxNode Fs) = Lean.Level.PP.Result.maxNode (x✝ :: Fs)
• x✝¹.max x✝ = Lean.Level.PP.Result.maxNode [x✝¹, x✝]

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

Equations

• x✝.imax (Lean.Level.PP.Result.imaxNode Fs) = Lean.Level.PP.Result.imaxNode (x✝ :: Fs)
• x✝¹.imax x✝ = Lean.Level.PP.Result.imaxNode [x✝¹, x✝]

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

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

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

Equations

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

instance Lean.Level.instToFormat : ToFormat Level

Equations

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

instance Lean.Level.instToString : ToString Level

Equations

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

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

Equations

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

instance Lean.Level.instQuoteMkStr1 : Quote Level `level

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• (a.max a_1).updateMax! newLhs newRhs = Lean.mkLevelMax' newLhs newRhs
• lvl.updateMax! newLhs newRhs = 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 newLhs newRhs : Level) : 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 Level → 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 : Level) (s : Name → Option Level) : Level

Equations

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

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

Equations

• Lean.Level.substParams.go s Lean.Level.zero = Lean.Level.zero
• Lean.Level.substParams.go s v.succ = if v.succ.hasParam = true then v.succ.updateSucc! (Lean.Level.substParams.go s v) else v.succ
• Lean.Level.substParams.go s (v₁.max v₂) = if (v₁.max v₂).hasParam = true then (v₁.max v₂).updateMax! (Lean.Level.substParams.go s v₁) (Lean.Level.substParams.go s v₂) else v₁.max v₂
• Lean.Level.substParams.go s (v₁.imax v₂) = if (v₁.imax v₂).hasParam = true then (v₁.imax v₂).updateIMax! (Lean.Level.substParams.go s v₁) (Lean.Level.substParams.go s v₂) else v₁.imax v₂
• 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 Name → List Level → Name → Option 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 : Level) (paramNames : List Name) (vs : List Level) : Level

Equations

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

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

Equations

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

@[irreducible]

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

@[reducible, inline]

abbrev Lean.LevelMap (α : Type) : Type

Equations

• Lean.LevelMap α = Std.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 = Std.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 : Level) (s : LMVarIdSet := ∅) : 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 : Level) (p : Level → Bool) : Option Level

Equations

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

def Lean.Level.find?.visit (p : Level → Bool) (u : Level) : Option 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 Lean.Level.find?.visit p u_2 <|> 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 Lean.Level.find?.visit p u_2 <|> 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 : Level) (p : 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