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.

Instances for level
@[protected, 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  :
@[protected, instance]
@[protected, instance]
meta def level.of_nat  :
meta def level.has_param  :
levelnamebool