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
@[instance]
meta def level.inhabited  :
inhabited level

source
@[instance]
meta constant level.has_decidable_eq  :
decidable_eq level

source
meta constant level.lt (a a_1 : level) :
bool

source
meta constant level.lex_lt (a a_1 : level) :
bool

source
meta constant level.fold {α : Type} (a : level) (a_1 : α) (a_2 : level → α → α) :
α

source
meta constant level.normalize (a : level) :
level

Return the given level expression normal form

source
meta constant level.eqv (a a_1 : level) :
bool

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

source
meta constant level.occurs (a a_1 : level) :
bool

Return tt iff the first level occurs in the second

source
meta constant level.instantiate (a : level) (a_1 : 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 (a : level) (a_1 : options) :
format

source
meta constant level.to_string (a : level) :
string

source
@[instance]
meta def level.has_to_string  :
has_to_string level

source
@[instance]
meta def level.has_to_format  :
has_to_format level

source
meta def level.of_nat (a : ℕ) :
level

source
meta def level.has_param (a : level) (a_1 : name) :
bool