Enum minitt::syntax::Value

pub enum Value {
    Lambda(Closure),
    Unit,
    One,
    Type,
    Pi(Box<Self>, Closure),
    Sigma(Box<Self>, Closure),
    Pair(Box<Self>, Box<Self>),
    Constructor(String, Box<Self>),
    Split(CaseTree),
    Sum(CaseTree),
    Neutral(Neutral),
}

Val in Mini-TT, value term.

Variants

Lambda(Closure)UnitOneTypePi(Box<Self>, Closure)Sigma(Box<Self>, Closure)Pair(Box<Self>, Box<Self>)Constructor(String, Box<Self>)Split(CaseTree)Sum(CaseTree)Neutral(Neutral)

Methods

impl Value

pub fn first(self) -> Value

vfst in Mini-TT.
Run .1 on a Pair.

pub fn second(self) -> Value

vsnd in Mini-TT.
Run .2 on a Pair.

pub fn destruct(self) -> (Value, Value)

Combination of vsnd and vfst in Mini-TT.
Run .2 on a Pair.

pub fn apply(self, argument: Value) -> Value

app in Mini-TT.

Trait Implementations

impl ReadBack for Value

type NormalForm = NormalExpression

Corresponding normal form type for the read-backable structures. This is needed because Rust does not support Higher-Kinded Types :(

fn read_back(self, index: u32) -> Self::NormalForm

rbV in Mini-TT.

fn eq_normal(self, index: u32, other: Self) -> Result<(), String>

eqNf in Mini-TT. Whether two structures are equivalent up to normal form.

impl Clone for Value

fn clone(&self) -> Value

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Display for Value

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

Formats the value using the given formatter.

impl Debug for Value

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

Formats the value using the given formatter.