mathlib3 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.

Instances for level
@[protected, instance]
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

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

meta constant level.to_string  :
@[protected, instance]
@[protected, instance]