Enum Val 

pub enum Val {
    Neu {
        kind: Kind,
        head: HeadId,
        spine: Sp,
    },
    Lam {
        dom: ExprId,
        env: EnvId,
        body: ExprId,
    },
    Pi {
        dom: V,
        env: EnvId,
        body: ExprId,
    },
    PiLam {
        dom: V,
        env: EnvId,
        ctx: CtxId,
        body: ExprId,
    },
    Sort(LevelId),
    Nat(NatId),
    Str(StrId),
}

Variants

Neu

Fields

kind: Kind

head: HeadId

spine: Sp

Lam

fun (x : dom) => body closed over env; the domain is evaluated on demand.

Fields

dom: ExprId

env: EnvId

body: ExprId

Pi

Fields

dom: V

env: EnvId

body: ExprId

PiLam

The type of a lambda: Π (x : dom), T where T is the type inferred for body in env and ctx extended by x — inferred only when something asks for the codomain.

Fields

dom: V

env: EnvId

ctx: CtxId

body: ExprId

Sort(LevelId)

Nat(NatId)

Str(StrId)

Trait Implementations

impl Clone for Val

fn clone(&self) -> Val

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Val

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

Formats the value using the given formatter.

impl PartialEq for Val

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

impl Eq for Val

impl StructuralPartialEq for Val