mathlib documentation

core / init.meta.level

source
meta inductive level  :
Type

A type universe term. eg max u v. Reflect a C++ level object. The VM replaces it with the C++ implementation.

source
@[protected, instance]
meta def level.inhabited  :
inhabited level
source
@[instance]
meta constant level.has_decidable_eq  :
decidable_eq level
source
meta constant level.lt  :
level → level → bool
source
meta constant level.lex_lt  :
level → level → bool
source
meta constant level.fold {α : Type} :
level → α → (level → α → α) → α
source
meta constant level.normalize  :
level → level

Return the given level expression normal form

source
meta constant level.eqv  :
level → level → bool

Return tt iff lhs and rhs denote the same level. The check is done by normalization.

source
meta constant level.occurs  :
level → level → bool

Return tt iff the first level occurs in the second

source
meta constant level.instantiate  :
level → list (name × level) → level

Replace a parameter named n with l in the first level if the list contains the pair (n, l)

source
meta constant level.to_format  :
level → options → format
source
meta constant level.to_string  :
level → string
source
@[protected, instance]
meta def level.has_to_string  :
has_to_string level
source
@[protected, instance]
meta def level.has_to_format  :
has_to_format level
source
meta def level.of_nat  :
ℕ → level
source
meta def level.has_param  :
level → name → bool