[−][src]Enum minitt::ast::Value
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.
InferredSum(Box<GenericBranch<Value>>)
Internally generated: inferred sum type.
Neutral(Neutral)
Neutral form.
Methods
impl Value
[src]
pub fn first(self) -> Value
[src]
vfst
in Mini-TT.
Run .1
on a Pair.
pub fn second(self) -> Value
[src]
vsnd
in Mini-TT.
Run .2
on a Pair.
pub fn destruct(self) -> (Value, Value)
[src]
Combination of vsnd
and vfst
in Mini-TT.
Run .2
on a Pair.
pub fn apply(self, argument: Value) -> Value
[src]
app
in Mini-TT.
Trait Implementations
impl ReadBack for Value
[src]
type NormalForm = NormalExpression
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 read_back_please(self) -> Self::NormalForm
[src]
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)
[src]
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. Read more
impl Clone for Value
[src]
fn clone(&self) -> Value
[src]
fn clone_from(&mut self, source: &Self)
1.0.0[src]
Performs copy-assignment from source
. Read more
impl Display for Value
[src]
impl Debug for Value
[src]
Auto Trait Implementations
Blanket Implementations
impl<T> ToString for T where
T: Display + ?Sized,
[src]
T: Display + ?Sized,
impl<T> From for T
[src]
impl<T, U> Into for T where
U: From<T>,
[src]
U: From<T>,
impl<T> ToOwned for T where
T: Clone,
[src]
T: Clone,
impl<T, U> TryFrom for T where
U: Into<T>,
[src]
U: Into<T>,
type Error = Infallible
The type returned in the event of a conversion error.
fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>
[src]
impl<T> Borrow for T where
T: ?Sized,
[src]
T: ?Sized,
impl<T> Any for T where
T: 'static + ?Sized,
[src]
T: 'static + ?Sized,
impl<T> BorrowMut for T where
T: ?Sized,
[src]
T: ?Sized,
fn borrow_mut(&mut self) -> &mut T
[src]
impl<T, U> TryInto for T where
U: TryFrom<T>,
[src]
U: TryFrom<T>,