Enum ErasedExpr 

pub enum ErasedExpr {
    Var(String),
    BVar(u32),
    Lam(Box<ErasedExpr>),
    App(Box<ErasedExpr>, Box<ErasedExpr>),
    Let(Box<ErasedExpr>, Box<ErasedExpr>),
    Const(String),
    Lit(u64),
    StrLit(String),
    TypeErased,
}

A kernel expression with type information erased.

Variants

Var(String)

Erased free variable.

BVar(u32)

Bound variable (de Bruijn index).

Lam(Box<ErasedExpr>)

Lambda without type annotation.

App(Box<ErasedExpr>, Box<ErasedExpr>)

Application.

Let(Box<ErasedExpr>, Box<ErasedExpr>)

Let binding without type.

Const(String)

Global constant reference.

Lit(u64)

Literal natural number.

StrLit(String)

String literal.

TypeErased

Placeholder for erased types (sorts, pi-types, etc.).

Trait Implementations

impl Clone for ErasedExpr

fn clone(&self) -> ErasedExpr

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ErasedExpr

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

Formats the value using the given formatter.

impl PartialEq for ErasedExpr

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

impl StructuralPartialEq for ErasedExpr