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

- n.imax m = if m = 0 then 0 else n.max m

Instances For

source
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

source
instance Lean.instInhabitedData :
Inhabited Level.Data
Equations

- Lean.instInhabitedData = inferInstanceAs (Inhabited UInt64)

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

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

Instances For

source
instance Lean.instBEqData :
BEq Level.Data
Equations

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

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

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

Instances For

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

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

Instances For

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

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

Instances For

source
@[extern lean_level_mk_data]
opaque Lean.Level.mkData (h : UInt64) (depth : Nat := 0) (hasMVar hasParam : Bool := false) :
Data
source
instance Lean.instReprData :
Repr Level.Data
Equations

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

source
structure Lean.LevelMVarId :
Type

Universe level metavariable Id

- name : Name

Instances For

source
instance Lean.instInhabitedLevelMVarId :
Inhabited LevelMVarId
Equations

- Lean.instInhabitedLevelMVarId = { default := Lean.instInhabitedLevelMVarId.default }

source
def Lean.instInhabitedLevelMVarId.default :
LevelMVarId
Equations

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

Instances For

source
instance Lean.instBEqLevelMVarId :
BEq LevelMVarId
Equations

- Lean.instBEqLevelMVarId = { beq := Lean.instBEqLevelMVarId.beq }

source
def Lean.instBEqLevelMVarId.beq :
LevelMVarId → LevelMVarId → Bool
Equations

- Lean.instBEqLevelMVarId.beq { name := a } { name := b } = (a == b)
- Lean.instBEqLevelMVarId.beq x✝¹ x✝ = false

Instances For

source
instance Lean.instHashableLevelMVarId :
Hashable LevelMVarId
Equations

- Lean.instHashableLevelMVarId = { hash := Lean.instHashableLevelMVarId.hash }

source
def Lean.instHashableLevelMVarId.hash :
LevelMVarId → UInt64
Equations

- Lean.instHashableLevelMVarId.hash { name := a } = mixHash 0 (hash a)

Instances For

source
def Lean.instReprLevelMVarId.repr :
LevelMVarId → Nat → Format
Equations

- Lean.instReprLevelMVarId.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "name" ++ Std.Format.text " := " ++ (Std.Format.nest 8 (repr x✝.name)).group) " }"

Instances For

source
instance Lean.instReprLevelMVarId :
Repr LevelMVarId
Equations

- Lean.instReprLevelMVarId = { reprPrec := Lean.instReprLevelMVarId.repr }

source
@[reducible, inline]
abbrev Lean.LMVarId :
Type

Short for `LevelMVarId`

Equations

- Lean.LMVarId = Lean.LevelMVarId

Instances For

source
instance Lean.instReprLMVarId :
Repr LMVarId
Equations

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

source
def Lean.LMVarIdSet :
Type
Equations

- Lean.LMVarIdSet = Std.TreeSet Lean.LMVarId fun (x1 x2 : Lean.LMVarId) => x1.name.quickCmp x2.name

Instances For

source
instance Lean.instInhabitedLMVarIdSet :
Inhabited LMVarIdSet
Equations

- Lean.instInhabitedLMVarIdSet = Std.TreeSet.instInhabited

source
instance Lean.instEmptyCollectionLMVarIdSet :
EmptyCollection LMVarIdSet
Equations

- Lean.instEmptyCollectionLMVarIdSet = Std.TreeSet.instEmptyCollection

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

- Lean.instForInLMVarIdSetLMVarId = inferInstanceAs (ForIn m (Std.TreeSet Lean.LMVarId fun (x1 x2 : Lean.LMVarId) => x1.name.quickCmp x2.name) Lean.LMVarId)

source
def Lean.LMVarIdMap (α : Type) :
Type
Equations

- Lean.LMVarIdMap α = Std.TreeMap Lean.LMVarId α fun (x1 x2 : Lean.LMVarId) => x1.name.quickCmp x2.name

Instances For

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

- Lean.instEmptyCollectionLMVarIdMap = inferInstanceAs (EmptyCollection (Std.TreeMap Lean.LMVarId α fun (x1 x2 : Lean.LMVarId) => x1.name.quickCmp x2.name))

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

- Lean.instForInLMVarIdMapProdLMVarId = inferInstanceAs (ForIn m (Std.TreeMap Lean.LMVarId α fun (x1 x2 : Lean.LMVarId) => x1.name.quickCmp x2.name) (Lean.LMVarId × α))

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

- Lean.instInhabitedLMVarIdMap = { default := ∅ }

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

Instances For

source
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

source
def Lean.instInhabitedLevel.default :
Level
Equations

- Lean.instInhabitedLevel.default = Lean.Level.zero

Instances For

source
instance Lean.instInhabitedLevel :
Inhabited Level
Equations

- Lean.instInhabitedLevel = { default := Lean.instInhabitedLevel.default }

source
instance Lean.instReprLevel :
Repr Level
Equations

- Lean.instReprLevel = { reprPrec := Lean.instReprLevel.repr }

source
def Lean.instReprLevel.repr :
Level → Nat → Format
Equations

- One or more equations did not get rendered due to their size.
- Lean.instReprLevel.repr Lean.Level.zero prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lean.Level.zero")).group prec✝

Instances For

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

- u.hash = u.data.hash

Instances For

source
instance Lean.Level.instHashable :
Hashable Level
Equations

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

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

- u.depth = u.data.depth.toNat

Instances For

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

- u.hasMVar = u.data.hasMVar

Instances For

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

- u.hasParam = u.data.hasParam

Instances For

source
@[export lean_level_hash]
def Lean.Level.hashEx (u : Level) :
UInt32
Equations

- u.hashEx = (hash u).toUInt32

Instances For

source
@[export lean_level_has_mvar]
def Lean.Level.hasMVarEx :
Level → Bool
Equations

- Lean.Level.hasMVarEx = Lean.Level.hasMVar

Instances For

source
@[export lean_level_has_param]
def Lean.Level.hasParamEx :
Level → Bool
Equations

- Lean.Level.hasParamEx = Lean.Level.hasParam

Instances For

source
@[export lean_level_depth]
def Lean.Level.depthEx (u : Level) :
UInt32
Equations

- u.depthEx = u.data.depth

Instances For

source
def Lean.levelZero :
Level
Equations

- Lean.levelZero = Lean.Level.zero

Instances For

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

- Lean.mkLevelMVar mvarId = Lean.Level.mvar mvarId

Instances For

source
def Lean.mkLevelParam (name : Name) :
Level
Equations

- Lean.mkLevelParam name = Lean.Level.param name

Instances For

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

- Lean.mkLevelSucc u = u.succ

Instances For

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

- Lean.mkLevelMax u v = u.max v

Instances For

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

- Lean.mkLevelIMax u v = u.imax v

Instances For

source
def Lean.levelOne :
Level
Equations

- Lean.levelOne = Lean.mkLevelSucc Lean.levelZero

Instances For

source
@[export lean_level_mk_zero]
def Lean.mkLevelZeroEx :
Unit → Level
Equations

- Lean.mkLevelZeroEx x✝ = Lean.levelZero

Instances For

source
@[export lean_level_mk_succ]
def Lean.mkLevelSuccEx :
Level → Level
Equations

- Lean.mkLevelSuccEx = Lean.mkLevelSucc

Instances For

source
@[export lean_level_mk_mvar]
def Lean.mkLevelMVarEx :
LMVarId → Level
Equations

- Lean.mkLevelMVarEx = Lean.mkLevelMVar

Instances For

source
@[export lean_level_mk_param]
def Lean.mkLevelParamEx :
Name → Level
Equations

- Lean.mkLevelParamEx = Lean.mkLevelParam

Instances For

source
@[export lean_level_mk_max]
def Lean.mkLevelMaxEx :
Level → Level → Level
Equations

- Lean.mkLevelMaxEx = Lean.mkLevelMax

Instances For

source
@[export lean_level_mk_imax]
def Lean.mkLevelIMaxEx :
Level → Level → Level
Equations

- Lean.mkLevelIMaxEx = Lean.mkLevelIMax

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

source
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

Instances For

source
def Lean.Level.isAlwaysZero :
Level → Bool

Returns true if and only if `l` evaluates to zero for all instantiations of parameters and meta-variables.

Equations

- Lean.Level.zero.isAlwaysZero = true
- (Lean.Level.param a).isAlwaysZero = false
- (Lean.Level.mvar a).isAlwaysZero = false
- a.succ.isAlwaysZero = false
- (l₁.max l₂).isAlwaysZero = (l₁.isAlwaysZero && l₂.isAlwaysZero)
- (a.imax l₂).isAlwaysZero = l₂.isAlwaysZero

Instances For

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

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

Instances For

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

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

source
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✝)

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

- lvl.getOffset = lvl.getOffsetAux 0

Instances For

source
def Lean.Level.getLevelOffset :
Level → Level
Equations

- a.succ.getLevelOffset = a.getLevelOffset
- x✝.getLevelOffset = x✝

Instances For

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

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

Instances For

source
@[extern lean_level_eq]
opaque Lean.Level.beq (a b : Level) :
Bool
source
instance Lean.Level.instBEq :
BEq Level
Equations

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

source
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✝)

Instances For

source
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

Instances For

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

Instances For

source
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

Instances For

source
def Lean.Level.isAlreadyNormalizedCheap :
Level → Bool
Equations

- Lean.Level.zero.isAlreadyNormalizedCheap = true
- (Lean.Level.param a).isAlreadyNormalizedCheap = true
- (Lean.Level.mvar a).isAlreadyNormalizedCheap = true
- u.succ.isAlreadyNormalizedCheap = u.isAlreadyNormalizedCheap
- x✝.isAlreadyNormalizedCheap = false

Instances For

source
partial def Lean.Level.normalize (l : Level) :
Level
source
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)

Instances For

source
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)

Instances For

source
inductive Lean.Level.PP.Result :
Type

- leaf : Name → Result
- num : Nat → Result
- offset : Result → Nat → Result
- maxNode : List Result → Result
- imaxNode : List Result → Result

Instances For

source
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

Instances For

source
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✝]

Instances For

source
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✝]

Instances For

source
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 `_

Instances For

source
partial def Lean.Level.PP.Result.format :
Result → Bool → Format
source
partial def Lean.Level.PP.Result.quote (r : Result) (prec : Nat) :
Syntax.Level
source
def Lean.Level.format (u : Level) (mvars : Bool) :
Format
Equations

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

Instances For

source
instance Lean.Level.instToFormat :
ToFormat Level
Equations

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

source
instance Lean.Level.instToString :
ToString Level
Equations

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

source
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

Instances For

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

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

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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.

source
@[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!" 557 14 "succ level expected"

Instances For

source
@[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!" 568 15 "max level expected"

Instances For

source
@[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!" 579 16 "imax level expected"

Instances For

source
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)

Instances For

source
@[specialize #[]]
def Lean.Level.substParams (u : Level) (s : Name → Option Level) :
Level
Equations

- u.substParams s = Lean.Level.substParams.go✝ s u

Instances For

source
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

Instances For

source
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)

Instances For

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

- u.geq v = Lean.Level.geq.go✝ u.normalize v.normalize

Instances For

source
@[reducible, inline]
abbrev Lean.LevelMap (α : Type) :
Type
Equations

- Lean.LevelMap α = Std.HashMap Lean.Level α

Instances For

source
@[reducible, inline]
abbrev Lean.PersistentLevelMap (α : Type) :
Type
Equations

- Lean.PersistentLevelMap α = Lean.PHashMap Lean.Level α

Instances For

source
@[reducible, inline]
abbrev Lean.LevelSet :
Type
Equations

- Lean.LevelSet = Std.HashSet Lean.Level

Instances For

source
@[reducible, inline]
abbrev Lean.PersistentLevelSet :
Type
Equations

- Lean.PersistentLevelSet = Lean.PHashSet Lean.Level

Instances For

source
@[reducible, inline]
abbrev Lean.PLevelSet :
Type
Equations

- Lean.PLevelSet = Lean.PersistentLevelSet

Instances For

source
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 = Std.TreeSet.insert s n
- u.collectMVars s = s

Instances For

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

- u.find? p = Lean.Level.find?.visit✝ p u

Instances For

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

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

Instances For

source
@[reducible, inline]
abbrev Nat.toLevel (n : Nat) :
Lean.Level
Equations

- n.toLevel = Lean.Level.ofNat n

Instances For