Lean.Level

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

Equations

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

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

source

instance Lean.instInhabitedData:

Inhabited Lean.Level.Data

Equations

Lean.instInhabitedData = inferInstanceAs (Inhabited UInt64)

source

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

UInt64

Equations

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

source

instance Lean.instBEqData:

BEq Lean.Level.Data

Equations

Lean.instBEqData = { beq := fun a b => a == b }

source

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

UInt32

Equations

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

source

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

Bool

Equations

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

source

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

Bool

Equations

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

source

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.

source

instance Lean.instReprData:

Repr Lean.Level.Data

Equations

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

source

structure Lean.MVarId:

Type

name : Lean.Name

source

instance Lean.instInhabitedMVarId:

Inhabited Lean.MVarId

Equations

Lean.instInhabitedMVarId = { default := { name := default } }

source

instance Lean.instBEqMVarId:

BEq Lean.MVarId

Equations

Lean.instBEqMVarId = { beq := [anonymous] }

source

instance Lean.instHashableMVarId:

Hashable Lean.MVarId

Equations

Lean.instHashableMVarId = { hash := [anonymous] }

source

instance Lean.instReprMVarId:

Repr Lean.MVarId

Equations

Lean.instReprMVarId = { reprPrec := [anonymous] }

source

instance Lean.instReprMVarId_1:

Repr Lean.MVarId

Equations

Lean.instReprMVarId_1 = { reprPrec := fun n p => reprPrec n.name p }

source

def Lean.MVarIdSet:

Type

Equations

Lean.MVarIdSet = Std.RBTree Lean.MVarId fun a a_1 => Lean.Name.quickCmp a.name a_1.name

source

instance Lean.instForInMVarIdSetMVarId {m : Type u_1 → Type u_2} :

ForIn m Lean.MVarIdSet Lean.MVarId

Equations

Lean.instForInMVarIdSetMVarId = inferInstanceAs (ForIn m (Std.RBTree Lean.MVarId fun a a_1 => Lean.Name.quickCmp a.name a_1.name) Lean.MVarId)

source

def Lean.MVarIdMap (α : Type) :

Type

Equations

Lean.MVarIdMap α = Std.RBMap Lean.MVarId α fun a a_1 => Lean.Name.quickCmp a.name a_1.name

source

instance Lean.instEmptyCollectionMVarIdMap {α : Type} :

EmptyCollection (Lean.MVarIdMap α)

Equations

Lean.instEmptyCollectionMVarIdMap = inferInstanceAs (EmptyCollection (Std.RBMap Lean.MVarId α fun a a_1 => Lean.Name.quickCmp a.name a_1.name))

source

instance Lean.instForInMVarIdMapProdMVarId {m : Type u_1 → Type u_2} {α : Type} :

ForIn m (Lean.MVarIdMap α) (Lean.MVarId × α)

Equations

Lean.instForInMVarIdMapProdMVarId = inferInstanceAs (ForIn m (Std.RBMap Lean.MVarId α fun a a_1 => Lean.Name.quickCmp a.name a_1.name) (Lean.MVarId × α))

source

instance Lean.instInhabitedMVarIdMap {α : Type} :

Inhabited (Lean.MVarIdMap α)

Equations

Lean.instInhabitedMVarIdMap = { default := ∅ }

source

inductive Lean.Level:

Type

zero: Lean.Level.Data → Lean.Level
succ: Lean.Level → Lean.Level.Data → Lean.Level
max: Lean.Level → Lean.Level → Lean.Level.Data → Lean.Level
imax: Lean.Level → Lean.Level → Lean.Level.Data → Lean.Level
param: Lean.Name → Lean.Level.Data → Lean.Level
mvar: Lean.MVarId → Lean.Level.Data → Lean.Level

source

instance Lean.instInhabitedLevel:

Inhabited Lean.Level

Equations

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

source

instance Lean.instReprLevel:

Repr Lean.Level

Equations

Lean.instReprLevel = { reprPrec := [anonymous] }

source

@[inline]

def Lean.Level.data:

Lean.Level → Lean.Level.Data

Equations

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

source

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

UInt64

Equations

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

source

instance Lean.Level.instHashableLevel:

Hashable Lean.Level

Equations

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

source

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

Nat

Equations

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

source

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

Bool

Equations

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

source

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

Bool

Equations

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

source

@[export lean_level_hash]

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

UInt32

Equations

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

source

@[export lean_level_has_mvar]

def Lean.Level.hasMVarEx:

Lean.Level → Bool

Equations

Lean.Level.hasMVarEx = Lean.Level.hasMVar

source

@[export lean_level_has_param]

def Lean.Level.hasParamEx:

Lean.Level → Bool

Equations

Lean.Level.hasParamEx = Lean.Level.hasParam

source

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

source

def Lean.levelZero:

Lean.Level

Equations

Lean.levelZero = Lean.Level.zero (Lean.Level.mkData 2221 0 false)

source

def Lean.mkLevelMVar (mvarId : Lean.MVarId) :

Lean.Level

Equations

Lean.mkLevelMVar mvarId = Lean.Level.mvar mvarId (Lean.Level.mkData (mixHash 2237 (hash mvarId)) 0 true)

source

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

Lean.Level

Equations

Lean.mkLevelParam name = Lean.Level.param name (Lean.Level.mkData (mixHash 2239 (hash name)) 0 false true)

source

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

Lean.Level

Equations

Lean.mkLevelSucc u = Lean.Level.succ u (Lean.Level.mkData (mixHash 2243 (hash u)) (Lean.Level.depth u + 1) (Lean.Level.hasMVar u) (Lean.Level.hasParam u))

source

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

Lean.Level

Equations

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

source

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

Lean.Level

Equations

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

source

def Lean.levelOne:

Lean.Level

Equations

Lean.levelOne = Lean.mkLevelSucc Lean.levelZero

source

@[export lean_level_mk_zero]

def Lean.mkLevelZeroEx:

Unit → Lean.Level

Equations

Lean.mkLevelZeroEx x = Lean.levelZero

source

@[export lean_level_mk_succ]

def Lean.mkLevelSuccEx:

Lean.Level → Lean.Level

Equations

Lean.mkLevelSuccEx = Lean.mkLevelSucc

source

@[export lean_level_mk_mvar]

def Lean.mkLevelMVarEx:

Lean.MVarId → Lean.Level

Equations

Lean.mkLevelMVarEx = Lean.mkLevelMVar

source

@[export lean_level_mk_param]

def Lean.mkLevelParamEx:

Lean.Name → Lean.Level

Equations

Lean.mkLevelParamEx = Lean.mkLevelParam

source

@[export lean_level_mk_max]

def Lean.mkLevelMaxEx:

Lean.Level → Lean.Level → Lean.Level

Equations

Lean.mkLevelMaxEx = Lean.mkLevelMax

source

@[export lean_level_mk_imax]

def Lean.mkLevelIMaxEx:

Lean.Level → Lean.Level → Lean.Level

Equations

Lean.mkLevelIMaxEx = Lean.mkLevelIMax

source

def Lean.Level.isZero:

Lean.Level → Bool

Equations

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

source

def Lean.Level.isSucc:

Lean.Level → Bool

Equations

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

source

def Lean.Level.isMax:

Lean.Level → Bool

Equations

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

source

def Lean.Level.isIMax:

Lean.Level → Bool

Equations

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

source

def Lean.Level.isMaxIMax:

Lean.Level → Bool

Equations

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

source

def Lean.Level.isParam:

Lean.Level → Bool

Equations

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

source

def Lean.Level.isMVar:

Lean.Level → Bool

Equations

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

source

def Lean.Level.mvarId!:

Lean.Level → Lean.MVarId

Equations

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

source

def Lean.Level.isNeverZero:

Lean.Level → Bool

If result is true, then forall assignments A which assigns all parameters and metavariables occuring in l, l[A] != zero

Equations

Lean.Level.isNeverZero (Lean.Level.zero a) = false
Lean.Level.isNeverZero (Lean.Level.param a a_1) = false
Lean.Level.isNeverZero (Lean.Level.mvar a a_1) = false
Lean.Level.isNeverZero (Lean.Level.succ a a_1) = true
Lean.Level.isNeverZero (Lean.Level.max l₁ l₂ a) = (Lean.Level.isNeverZero l₁ || Lean.Level.isNeverZero l₂)
Lean.Level.isNeverZero (Lean.Level.imax a l₂ a_1) = Lean.Level.isNeverZero l₂

source

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)

source

def Lean.Level.addOffsetAux:

Nat → Lean.Level → Lean.Level

Equations

Lean.Level.addOffsetAux 0 _fun_discr = _fun_discr
Lean.Level.addOffsetAux (Nat.succ n) _fun_discr = Lean.Level.addOffsetAux n (Lean.mkLevelSucc _fun_discr)

source

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

Lean.Level

Equations

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

source

def Lean.Level.isExplicit:

Lean.Level → Bool

source

def Lean.Level.getOffsetAux:

Lean.Level → Nat → Nat

Equations

Lean.Level.getOffsetAux (Lean.Level.succ u a) _fun_discr = Lean.Level.getOffsetAux u (_fun_discr + 1)
Lean.Level.getOffsetAux _fun_discr _fun_discr = _fun_discr

source

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

Nat

Equations

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

source

def Lean.Level.getLevelOffset:

Lean.Level → Lean.Level

Equations

Lean.Level.getLevelOffset (Lean.Level.succ a a_1) = Lean.Level.getLevelOffset a
Lean.Level.getLevelOffset _fun_discr = _fun_discr

source

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

Option Nat

Equations

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

source

@[extern lean_level_eq]

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

Bool

source

instance Lean.Level.instBEqLevel:

BEq Lean.Level

Equations

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

source

def Lean.Level.occurs:

Lean.Level → Lean.Level → Bool

occurs u l return true iff u occurs in l.

Equations

Lean.Level.occurs _fun_discr (Lean.Level.succ v₁ a) = (_fun_discr == Lean.Level.succ v₁ a || Lean.Level.occurs _fun_discr v₁)
Lean.Level.occurs _fun_discr (Lean.Level.max v₁ v₂ a) = (_fun_discr == Lean.Level.max v₁ v₂ a || Lean.Level.occurs _fun_discr v₁ || Lean.Level.occurs _fun_discr v₂)
Lean.Level.occurs _fun_discr (Lean.Level.imax v₁ v₂ a) = (_fun_discr == Lean.Level.imax v₁ v₂ a || Lean.Level.occurs _fun_discr v₁ || Lean.Level.occurs _fun_discr v₂)
Lean.Level.occurs _fun_discr _fun_discr = (_fun_discr == _fun_discr)

source

def Lean.Level.ctorToNat:

Lean.Level → Nat

Equations

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

source

partial def Lean.Level.normLtAux:

Lean.Level → Nat → Lean.Level → Nat → Bool

source

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

source

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

Lean.Level

source

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

Bool

Equations

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

source

def Lean.Level.dec:

Lean.Level → Option Lean.Level

Reduce (if possible) universe level by 1

Equations

Lean.Level.dec (Lean.Level.zero a) = none
Lean.Level.dec (Lean.Level.param a a_1) = none
Lean.Level.dec (Lean.Level.mvar a a_1) = none
Lean.Level.dec (Lean.Level.succ a a_1) = some a
Lean.Level.dec (Lean.Level.max l₁ l₂ a) = do let a ← Lean.Level.dec l₁ let a_1 ← Lean.Level.dec l₂ pure (Lean.mkLevelMax a a_1)
Lean.Level.dec (Lean.Level.imax a l₂ a_1) = do let a ← Lean.Level.dec a let a_1 ← Lean.Level.dec l₂ pure (Lean.mkLevelMax a a_1)

source

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

source

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.

source

def Lean.Level.PP.Result.max:

Lean.Level.PP.Result → Lean.Level.PP.Result → Lean.Level.PP.Result

Equations

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

source

def Lean.Level.PP.Result.imax:

Lean.Level.PP.Result → Lean.Level.PP.Result → Lean.Level.PP.Result

Equations

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

source

def Lean.Level.PP.toResult:

Lean.Level → Lean.Level.PP.Result

Equations

Lean.Level.PP.toResult (Lean.Level.zero a) = Lean.Level.PP.Result.num 0
Lean.Level.PP.toResult (Lean.Level.succ a a_1) = Lean.Level.PP.Result.succ (Lean.Level.PP.toResult a)
Lean.Level.PP.toResult (Lean.Level.max a a_1 a_2) = 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 a_2) = Lean.Level.PP.Result.imax (Lean.Level.PP.toResult a) (Lean.Level.PP.toResult a_1)
Lean.Level.PP.toResult (Lean.Level.param a a_1) = Lean.Level.PP.Result.leaf a
Lean.Level.PP.toResult (Lean.Level.mvar a a_1) = let n := Lean.Name.replacePrefix a.name `_uniq (Lean.Name.mkSimple "?u"); Lean.Level.PP.Result.leaf n

source

partial def Lean.Level.PP.Result.format:

Lean.Level.PP.Result → Bool → Lean.Format

source

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

Lean.Syntax.Level

source

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

source

instance Lean.Level.instToFormatLevel:

Lean.ToFormat Lean.Level

Equations

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

source

instance Lean.Level.instToStringLevel:

ToString Lean.Level

Equations

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

source

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

source

instance Lean.Level.instQuoteLevelMkStrAnonymous:

Lean.Quote Lean.Level `level

Equations

Lean.Level.instQuoteLevelMkStrAnonymous = Lean.Quote.mk `level fun u => Lean.Level.quote u

source

@[export lean_level_mk_max_simp]

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

Lean.Level

Equations

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

source

@[export lean_level_mk_imax_simp]

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

Lean.Level

Equations

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

source

@[extern lean_level_update_succ]

def Lean.Level.updateSucc (lvl : Lean.Level) (newLvl : Lean.Level) (h : Lean.Level.isSucc lvl = true) :

Lean.Level

Equations

Lean.Level.updateSucc lvl newLvl h = Lean.mkLevelSucc newLvl

source

@[inline]

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.

source

@[extern lean_level_update_max]

def Lean.Level.updateMax (lvl : Lean.Level) (newLhs : Lean.Level) (newRhs : Lean.Level) (h : Lean.Level.isMax lvl = true) :

Lean.Level

Equations

Lean.Level.updateMax lvl newLhs newRhs h = Lean.mkLevelMax' newLhs newRhs

source

@[inline]

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.

source

@[extern lean_level_update_imax]

def Lean.Level.updateIMax (lvl : Lean.Level) (newLhs : Lean.Level) (newRhs : Lean.Level) (h : Lean.Level.isIMax lvl = true) :

Lean.Level

Equations

Lean.Level.updateIMax lvl newLhs newRhs h = Lean.mkLevelIMax' newLhs newRhs

source

@[inline]

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.

source

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)

source

@[specialize]

def Lean.Level.instantiateParams (s : Lean.Name → Option Lean.Level) :

Lean.Level → Lean.Level

Equations

One or more equations did not get rendered due to their size.
Lean.Level.instantiateParams s (Lean.Level.zero a) = Lean.Level.zero a
Lean.Level.instantiateParams s (Lean.Level.param n a) = match s n with | some u' => u' | none => Lean.Level.param n a
Lean.Level.instantiateParams s _fun_discr = _fun_discr

source

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)

source

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

Bool

source

@[inline]

abbrev Lean.LevelMap (α : Type) :

Type

Equations

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

source

@[inline]

abbrev Lean.PersistentLevelMap (α : Type) :

Type

Equations

Lean.PersistentLevelMap α = Std.PHashMap Lean.Level α

source

@[inline]

abbrev Lean.LevelSet:

Type

Equations

Lean.LevelSet = Std.HashSet Lean.Level

source

@[inline]

abbrev Lean.PersistentLevelSet:

Type

Equations

Lean.PersistentLevelSet = Std.PHashSet Lean.Level

source

@[inline]

abbrev Lean.PLevelSet:

Type

Equations

Lean.PLevelSet = Lean.PersistentLevelSet

source

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

Lean.MVarIdSet

Equations

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

source

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

source

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 a) = if p (Lean.Level.succ v a) = true then pure (Lean.Level.succ v a) else Lean.Level.find?.visit p v
Lean.Level.find?.visit p u = if p u = true then pure u else failure

source

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)

source

@[inline]

abbrev Nat.toLevel (n : Nat) :

Lean.Level

Equations

Nat.toLevel n = Lean.Level.ofNat n