[−][src]Enum minitt::ast::Value
Val
in Mini-TT, value term.
Terms are either of canonical form or neutral form.
$u,v,t ::=$
Variants
Lambda(Closure)
$\lambda\ f$. Canonical form: lambda abstraction.
$0$. Canonical form: unit instance.
$\textbf{1}$. Canonical form: unit type.
Type(Level)
$\textsf{U}$. Canonical form: type universe.
$\Pi \ t\ g$. Canonical form: pi type (type for dependent functions).
$\Sigma \ t\ g$. Canonical form: sigma type (type for dependent pair).
$u,v$. Canonical form: Pair value (value for sigma).
$c \ t$. Canonical form: call to a constructor.
Split(CaseTree)
$\textsf{fun}\ s$. Canonical form: case-split.
Sum(CaseTree)
$\textsf{Sum}\ s$. Canonical form: sum type.
Neutral(Neutral)
$[k]$. Neutral form.
Methods
impl Value
[src]
pub fn level_safe(&self) -> Option<Level>
[src]
This is not present in Mini-TT.
Calculate the level of self
, return None
if it's not a type value.
pub fn level(&self) -> u32
[src]
This is not present in Mini-TT.
This is called levelView
in Agda.
pub fn first(self) -> Self
[src]
$$
\begin{alignedat}{2}
& (u,v).1 &&= u \\
& [k].1 &&= [k.1] \\
\end{alignedat}
$$
vfst
in Mini-TT.
Run .1
on a Pair.
pub fn second(self) -> Self
[src]
$$
\begin{alignedat}{2}
& (u,v).2 &&= v \\
& [k].2 &&= [k.2] \\
\end{alignedat}
$$
vsnd
in Mini-TT.
Run .2
on a Pair.
pub fn destruct(self) -> (Self, Self)
[src]
Combination of vsnd
and vfst
in Mini-TT.
Run .2
on a Pair.
pub fn apply(self, argument: Self) -> Self
[src]
$$
\begin{alignedat}{2}
& \textsf{app} (\lambda \ f) v &&= \textsf{inst} \ f \ v \\
& \textsf{app} (\textsf{fun}\lang S,\rho \rang (c_i \ v)) &&=
\textsf{app}(⟦ M_i ⟧ \rho)v \\
& && \ \ \ \ \ \ \textnormal{where}
\ S=(c_1 \rightarrow M_1 | ... | c_n \rightarrow M_n) \\
& \textsf{app} (\textsf{fun} \ s) [k] &&= [s \ k] \\
& \textsf{app} [k] \ v &&= [k \ v]
\end{alignedat}
$$
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]
$$
\begin{alignedat}{2}
& \textsf{R}_i (\lambda \ f) &&= \lambda \ \textsf{x}_i
\ . \ \textsf{R}_{i+1} (\textsf{inst}\ f [ \textsf{x}_i ]) \\
& \textsf{R}_i (u,v) &&= (\textsf{R}_i u,\textsf{R}_i v) \\
& \textsf{R}_i 0 &&= 0 \\
& \textsf{R}_i (c\ v) &&= c \ (\textsf{R}_i v) \\
& \textsf{R}_i (\textsf{fun}\lang S,\rho\rang) &&= \textsf{fun}\lang S,
\textsf{R}_i \rho\rang \\
& \textsf{R}_i (\textsf{Sum}\lang S,\rho\rang) &&= \textsf{Sum}\lang S,
\textsf{R}_i \rho\rang \\
& \textsf{R}_i \textsf{U} &&= \textsf{U} \\
& \textsf{R}_i \textbf{1} &&= \textbf{1} \\
& \textsf{R}_i (\Pi\ t\ g) &&= \Pi \textsf{x}_i : \textsf{R}_i \ t
\ . \ \textsf{R}_{i+1} (\textsf{inst}\ g [ \textsf{x}_i ]) \\
& \textsf{R}_i (\Sigma\ t\ g) &&= \Sigma \textsf{x}_i : \textsf{R}_i \ t
\ . \ \textsf{R}_{i+1} (\textsf{inst}\ g [ \textsf{x}_i ]) \\
& \textsf{R}_i [k] &&= [\textsf{R}_i\ k]
\end{alignedat}
$$
rbV
in Mini-TT.
fn read_back_please(self) -> Self::NormalForm
[src]
fn normal(
index: u32,
me: Self,
other: Self
) -> (Self::NormalForm, Self::NormalForm)
[src]
index: u32,
me: Self,
other: Self
) -> (Self::NormalForm, Self::NormalForm)
impl Clone for Value
[src]
impl Debug for Value
[src]
impl Display for Value
[src]
Auto Trait Implementations
impl !Sync for Value
impl !Send for Value
impl Unpin for Value
impl !UnwindSafe for Value
impl !RefUnwindSafe for Value
Blanket Implementations
impl<T, U> Into<U> for T where
U: From<T>,
[src]
U: From<T>,
impl<T> ToString for T where
T: Display + ?Sized,
[src]
T: Display + ?Sized,
impl<T> ToOwned for T where
T: Clone,
[src]
T: Clone,
type Owned = T
The resulting type after obtaining ownership.
fn to_owned(&self) -> T
[src]
fn clone_into(&self, target: &mut T)
[src]
impl<T> From<T> for T
[src]
impl<T, U> TryFrom<U> 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, U> TryInto<U> for T where
U: TryFrom<T>,
[src]
U: TryFrom<T>,
type Error = <U as TryFrom<T>>::Error
The type returned in the event of a conversion error.
fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>
[src]
impl<T> BorrowMut<T> for T where
T: ?Sized,
[src]
T: ?Sized,
fn borrow_mut(&mut self) -> &mut T
[src]
impl<T> Borrow<T> for T where
T: ?Sized,
[src]
T: ?Sized,
impl<T> Any for T where
T: 'static + ?Sized,
[src]
T: 'static + ?Sized,