Enum TermKind 

pub enum TermKind {
    Sort(LevelId),
    Const(SymbolId, Vec<LevelId>),
    Var(u32),
    App(TermId, TermId),
    Lam(Binder, TermId),
    Pi(Binder, TermId),
    Let(Binder, TermId, TermId),
    MVar(MetaVarId),
    Lit(Literal),
}

Core term representation

Variants

Sort(LevelId)

Universe sort (Type u)

Const(SymbolId, Vec<LevelId>)

Constant reference (name + universe parameters)

Var(u32)

Bound variable (de Bruijn index)

App(TermId, TermId)

Application (f x)

Lam(Binder, TermId)

Lambda abstraction (λ x : τ, body)

Pi(Binder, TermId)

Dependent function type (Π x : τ, body) / forall

Let(Binder, TermId, TermId)

Let binding (let x : τ := v in body)

MVar(MetaVarId)

Metavariable (hole to be filled during elaboration)

Lit(Literal)

Literal values (for optimization)

Trait Implementations

impl Clone for TermKind

fn clone(&self) -> TermKind

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for TermKind

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

Formats the value using the given formatter.

impl Display for TermKind

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

Formats the value using the given formatter.

impl Hash for TermKind

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl PartialEq for TermKind

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

impl StructuralPartialEq for TermKind