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

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

@[implicit_reducible]

instance Lean.instInhabitedData : Inhabited Level.Data

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

@[implicit_reducible]

instance Lean.instBEqData : BEq Level.Data

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

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

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

@[extern lean_level_mk_data]

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

@[implicit_reducible]

instance Lean.instReprData : Repr Level.Data

structure Lean.LevelMVarId : Type

Universe level metavariable Id

• name : Name

@[implicit_reducible]

instance Lean.instInhabitedLevelMVarId : Inhabited LevelMVarId

def Lean.instInhabitedLevelMVarId.default : LevelMVarId

@[implicit_reducible]

instance Lean.instBEqLevelMVarId : BEq LevelMVarId

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

@[implicit_reducible]

instance Lean.instHashableLevelMVarId : Hashable LevelMVarId

def Lean.instHashableLevelMVarId.hash : LevelMVarId → UInt64

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

@[implicit_reducible]

instance Lean.instReprLevelMVarId : Repr LevelMVarId

@[reducible, inline]

abbrev Lean.LMVarId : Type

Short for LevelMVarId

@[implicit_reducible]

instance Lean.instReprLMVarId : Repr LMVarId

def Lean.LMVarIdSet : Type

@[implicit_reducible]

instance Lean.instInhabitedLMVarIdSet : Inhabited LMVarIdSet

@[implicit_reducible]

instance Lean.instEmptyCollectionLMVarIdSet : EmptyCollection LMVarIdSet

@[implicit_reducible]

instance Lean.instForInLMVarIdSetLMVarIdOfMonad {m : Type u_1 → Type u_2} [Monad m] : ForIn m LMVarIdSet LMVarId

def Lean.LMVarIdMap (α : Type) : Type

@[implicit_reducible]

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

@[implicit_reducible]

instance Lean.instForInLMVarIdMapProdLMVarIdOfMonad {m : Type u_1 → Type u_2} {α : Type} [Monad m] : ForIn m (LMVarIdMap α) (LMVarId × α)

@[implicit_reducible]

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

@[implemented_by Lean.Level.data._override]

noncomputable def Lean.Level.data : Level → Data

inductive Lean.Level : Type

• zero : Level
• succ : Level → Level
• max : Level → Level → Level
• imax : Level → Level → Level
• param : Name → Level
• mvar : LMVarId → Level

def Lean.instInhabitedLevel.default : Level

@[implicit_reducible]

instance Lean.instInhabitedLevel : Inhabited Level

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

@[implicit_reducible]

instance Lean.instReprLevel : Repr Level

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

@[implicit_reducible]

instance Lean.Level.instHashable : Hashable Level

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

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

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

@[export lean_level_hash]

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

@[export lean_level_has_mvar]

def Lean.Level.hasMVarEx : Level → Bool

@[export lean_level_has_param]

def Lean.Level.hasParamEx : Level → Bool

@[export lean_level_depth]

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

@[implicit_reducible]

def Lean.levelZero : Level

def Lean.mkLevelMVar (mvarId : LMVarId) : Level

def Lean.mkLevelParam (name : Name) : Level

def Lean.mkLevelSucc (u : Level) : Level

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

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

def Lean.levelOne : Level

@[export lean_level_mk_zero]

def Lean.mkLevelZeroEx : Unit → Level

@[export lean_level_mk_succ]

def Lean.mkLevelSuccEx : Level → Level

@[export lean_level_mk_mvar]

def Lean.mkLevelMVarEx : LMVarId → Level

@[export lean_level_mk_param]

def Lean.mkLevelParamEx : Name → Level

@[export lean_level_mk_max]

def Lean.mkLevelMaxEx : Level → Level → Level

@[export lean_level_mk_imax]

def Lean.mkLevelIMaxEx : Level → Level → Level

def Lean.Level.isZero : Level → Bool

def Lean.Level.isSucc : Level → Bool

def Lean.Level.isMax : Level → Bool

def Lean.Level.isIMax : Level → Bool

def Lean.Level.isMaxIMax : Level → Bool

def Lean.Level.isParam : Level → Bool

def Lean.Level.isMVar : Level → Bool

def Lean.Level.mvarId! : Level → LMVarId

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

def Lean.Level.isAlwaysZero : Level → Bool

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

@[implicit_reducible]

def Lean.Level.ofNat : Nat → Level

@[implicit_reducible]

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

def Lean.Level.addOffsetAux : Nat → Level → Level

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

def Lean.Level.isExplicit : Level → Bool

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

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

def Lean.Level.getLevelOffset : Level → Level

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

@[extern lean_level_eq]

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

@[implicit_reducible]

instance Lean.Level.instBEq : BEq Level

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

occurs u l return true iff u occurs in l.

def Lean.Level.ctorToNat : Level → Nat

@[irreducible]

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

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.

def Lean.Level.isAlreadyNormalizedCheap : Level → Bool

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.

def Lean.Level.dec : Level → Option Level

Reduce (if possible) universe level by 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

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

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

def Lean.Level.PP.toResult (l : Level) (mvars : Bool) : Result

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

@[implicit_reducible]

instance Lean.Level.instToFormat : ToFormat Level

@[implicit_reducible]

instance Lean.Level.instToString : ToString Level

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

@[implicit_reducible]

instance Lean.Level.instQuoteMkStr1 : Quote Level `level

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

Similar to mkLevelMax, but applies cheap simplifications

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

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

Similar to mkLevelIMax, but applies cheap simplifications

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

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

@[implemented_by _private.Lean.Level.0.Lean.Level.updateMax!Impl]

def Lean.Level.updateMax! (lvl newLhs newRhs : Level) : Level

@[implemented_by _private.Lean.Level.0.Lean.Level.updateIMax!Impl]

def Lean.Level.updateIMax! (lvl newLhs newRhs : Level) : Level

def Lean.Level.mkNaryMax : List Level → Level

@[specialize #[]]

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

def Lean.Level.getParamSubst : List Name → List Level → Name → Option Level

def Lean.Level.instantiateParams (u : Level) (paramNames : List Name) (vs : List Level) : Level

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

@[reducible, inline]

abbrev Lean.LevelMap (α : Type) : Type

@[reducible, inline]

abbrev Lean.PersistentLevelMap (α : Type) : Type

@[reducible, inline]

abbrev Lean.LevelSet : Type

@[reducible, inline]

abbrev Lean.PersistentLevelSet : Type

@[reducible, inline]

abbrev Lean.PLevelSet : Type

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

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

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

@[reducible, inline]

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