Enum Universe 

pub enum Universe {
    Prop,
    Type(u32),
}

Universe levels in the type hierarchy.

The hierarchy is: Prop : Type 1 : Type 2 : Type 3 : …

• Prop is the universe of propositions (proof-irrelevant in full CIC)
• Type(n) is the universe of types at level n

Variants

Prop

Prop - the universe of propositions

Type(u32)

Type n - the universe of types at level n

Implementations

impl Universe

pub fn succ(&self) -> Universe

Get the successor universe: Type n → Type (n+1)

pub fn max(&self, other: &Universe) -> Universe

Get the maximum of two universes (for Pi type formation)

pub fn is_subtype_of(&self, other: &Universe) -> bool

Check if this universe is a subtype of another (cumulativity).

Subtyping rules:

• Prop ≤ Type(i) for all i
• Type(i) ≤ Type(j) if i ≤ j
• Type(i) is NOT ≤ Prop

Trait Implementations

impl Clone for Universe

fn clone(&self) -> Universe

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Universe

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

Formats the value using the given formatter.

impl Display for Universe

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

Formats the value using the given formatter.

impl PartialEq for Universe

fn eq(&self, other: &Universe) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Eq for Universe

impl StructuralPartialEq for Universe