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

Functions

calc_hash_map_level
calc_slice_level
calc_slice_plus_one_level
calc_tree_map_level
calc_tree_map_plus_one_level
lift_hash_map
lift_tree_map

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