mathlib documentation

core / init.meta.level

meta inductive level  :

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



meta constant  :

meta constant level.lex_lt  :

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

meta constant level.normalize  :

Return the given level expression normal form

meta constant level.eqv  :

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

meta constant level.occurs  :

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  :



meta def level.of_nat  :

meta def level.has_param  :