Enum minitt::ast::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.
Terms are either of canonical form or neutral form.

Variants

Lambda(Closure)

Canonical form: lambda abstraction.

Unit

Canonical form: unit instance.

One

Canonical form: unit type.

Type

Canonical form: type universe.

Pi(Box<Self>, Closure)

Canonical form: pi type (type for dependent functions).

Sigma(Box<Self>, Closure)

Canonical form: sigma type (type for dependent pair).

Pair(Box<Self>, Box<Self>)

Canonical form: Pair value (value for sigma).

Constructor(String, Box<Self>)

Canonical form: call to a constructor.

Split(CaseTree)

Canonical form: case-split.

Sum(CaseTree)

Canonical form: sum type.

Neutral(Neutral)

Neutral form.

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 read_back_please(self) -> Self::NormalForm

Sometimes you don't want to pass an argument, and let me do this for you :)

fn normal(
    index: u32,
    me: Self,
    other: Self
) -> (Self::NormalForm, Self::NormalForm)

eqNf in Mini-TT, but returning normal forms for error reporting. 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.