mathlib documentation

core.init.meta.level

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.

@[instance]

@[instance]

meta constant level.lt  :
levellevelbool

meta constant level.lex_lt  :
levellevelbool

meta constant level.fold {α : Type} :
levelα → (levelα → α) → α

meta constant level.normalize  :

Return the given level expression normal form

meta constant level.eqv  :
levellevelbool

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

meta constant level.occurs  :
levellevelbool

Return tt iff the first level occurs in the second

meta constant level.instantiate  :

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

meta constant level.to_format  :

meta constant level.to_string  :

@[instance]

@[instance]

meta def level.of_nat  :

meta def level.has_param  :
levelnamebool