[−][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((Box<BTreeMap<Name, Box<Expression<Name>>>>, Box<Telescope<Name>>)),
    Sum((Box<BTreeMap<Name, Box<Expression<Name>>>>, Box<Telescope<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((Box<BTreeMap<Name, Box<Expression<Name>>>>, Box<Telescope<Name>>))Sum((Box<BTreeMap<Name, Box<Expression<Name>>>>, Box<Telescope<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 apply(self, argument: Value<Name>) -> Value<Name>[src]

app in Mini-TT.

Trait Implementations

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> where
    Name: Send, 

impl<Name> Sync for Value<Name> where
    Name: Sync, 

Blanket Implementations

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> From for T[src]

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.