Module voile_util::level

Level-related definitions and relevant operations and traits.

Enums

Level

Level, can be inferred or user-specified.

Traits

LiftEx

Expression with universe level (which means they can be lifted).

Type Definitions

LevelCalcState

Internal API, public only because it's used in public traits' internal APIs. Produced during level calculation. Some(Level) -- level of non-recursive definitions. None -- level of self-reference. Trying to lift this will result in omega, otherwise it should be computed as 0 level.