[−][src]Enum minitt::syntax::Value

pub enum Value<Name: NameTrait> {
    Lambda(Closure<Name>),
    Unit,
    One,
    Type,
    Pi(Box<Value<Name>>, Closure<Name>),
    Sigma(Box<Value<Name>>, Closure<Name>),
    Pair(Box<Value<Name>>, Box<Value<Name>>),
    Constructor(Name, Box<Value<Name>>),
    Function(DeepClosure<Name>),
    Sum(DeepClosure<Name>),
    Neutral(Neutral<Name>),
}

Val in Mini-TT, value term.

Variants

Lambda(Closure<Name>)UnitOneTypePi(Box<Value<Name>>, Closure<Name>)Sigma(Box<Value<Name>>, Closure<Name>)Pair(Box<Value<Name>>, Box<Value<Name>>)Constructor(Name, Box<Value<Name>>)Function(DeepClosure<Name>)Sum(DeepClosure<Name>)Neutral(Neutral<Name>)

Methods

impl<Name: DebuggableNameTrait> Value<Name>[src]

pub fn first(self) -> Value<Name>[src]

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

pub fn second(self) -> Value<Name>[src]

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

pub fn destruct(self) -> (Value<Name>, Value<Name>)[src]

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

pub fn apply(self, argument: Value<Name>) -> Value<Name>[src]

app in Mini-TT.

Trait Implementations

impl<Name: DebuggableNameTrait> ReadBack for Value<Name>[src]

type NormalForm = NormalExpression<Name>

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

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

rbV in Mini-TT.

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

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

impl<Name: Clone + NameTrait> Clone for Value<Name>[src]

fn clone_from(&mut self, source: &Self)
1.0.0
[src]

Performs copy-assignment from source. Read more

impl<Name: Debug + NameTrait> Debug for Value<Name>[src]

Auto Trait Implementations

impl<Name> !Send for Value<Name>

impl<Name> !Sync for Value<Name>

Blanket Implementations

impl<T> From for T[src]

impl<T, U> Into for T where
    U: From<T>, [src]

impl<T> ToOwned for T where
    T: Clone, [src]

type Owned = T

impl<T, U> TryFrom for T where
    U: Into<T>, [src]

type Error = !

🔬 This is a nightly-only experimental API. (try_from)

The type returned in the event of a conversion error.

impl<T> Borrow for T where
    T: ?Sized, [src]

impl<T> Any for T where
    T: 'static + ?Sized, [src]

impl<T> BorrowMut for T where
    T: ?Sized, [src]

impl<T, U> TryInto for T where
    U: TryFrom<T>, [src]

type Error = <U as TryFrom<T>>::Error

🔬 This is a nightly-only experimental API. (try_from)

The type returned in the event of a conversion error.