Enum LevelView 

pub enum LevelView<'a> {
    SProp,
    Prop,
    Type(u32),
    Var(&'a str),
    Succ(LevelId),
    Max(LevelId, LevelId),
    IMax(LevelId, LevelId),
}

A borrowed view of one interned universe level.

Child handles belong to this store. Reading a view does not extract, clone, normalize, or recursively visit its payload.

Variants

SProp

The strict proposition universe.

Prop

The proposition universe.

Type(u32)

A concrete type universe.

Var(&'a str)

A borrowed universe variable name.

Succ(LevelId)

Successor of an interned level.

Max(LevelId, LevelId)

Maximum of two interned levels.

IMax(LevelId, LevelId)

Impredicative maximum of two interned levels.

Trait Implementations

impl<'a> Clone for LevelView<'a>

fn clone(&self) -> LevelView<'a>

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<'a> Debug for LevelView<'a>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<'a> Copy for LevelView<'a>