Enum TypeKind 

pub enum TypeKind {
    Prop,
    Type0,
    LargeType,
    Universe,
    Pi,
    Lambda,
    Application,
    FreeVar,
    Constant,
    Literal,
    Unknown,
}

Type-level kind classification of an expression.

Variants

Prop

A proposition (Sort 0 / Prop).

Type0

A small type (Sort 1, i.e., Type 0).

LargeType

A large type (Sort n for n ≥ 2).

Universe

A universe Sort expression itself.

Pi

A function type (Pi).

Lambda

A lambda (not a type).

Application

An application (not directly a type).

FreeVar

A free variable.

Constant

A constant.

Literal

A literal value.

Unknown

Unknown or uncategorized.

Trait Implementations

impl Clone for TypeKind

fn clone(&self) -> TypeKind

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for TypeKind

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

Formats the value using the given formatter.

impl PartialEq for TypeKind

fn eq(&self, other: &TypeKind) -> 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 Copy for TypeKind

impl Eq for TypeKind

impl StructuralPartialEq for TypeKind