Enum LevelView 

pub enum LevelView<'a> {
    Zero,
    Succ(&'a Level),
    Max(&'a Level, &'a Level),
    IMax(&'a Level, &'a Level),
    Param(&'a Name),
    MVar(LevelMVarId),
}

A borrowed view of a Level’s outermost node, for pattern matching.

Obtained from Level::view; mirrors the former public Level enum shape.

Variants

Zero

Level 0 (Prop).

Succ(&'a Level)

Successor: u + 1.

Max(&'a Level, &'a Level)

Maximum of two levels: max(u, v).

IMax(&'a Level, &'a Level)

Impredicative maximum: imax(u, v).

Param(&'a Name)

Universe parameter (for polymorphism).

MVar(LevelMVarId)

Universe metavariable (for unification).