Type Definition minitt::ast::Neutral

type Neutral = GenericNeutral<Value>;

$k ::= k(v)$. Neut in Mini-TT, neutral value.

Trait Implementations

impl ReadBack for Neutral

type NormalForm = NormalNeutral

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

$$ \begin{alignedat}{2} & \textsf{R}_i \textsf{x}_j &&= \textsf{x}_j \\ & \textsf{R}_i (k\ v) &&= (\textsf{R}_i\ k) (\textsf{R}_i\ v) \\ & \textsf{R}_i (k.1) &&= (\textsf{R}_i\ k) .1 \\ & \textsf{R}_i (k.2) &&= (\textsf{R}_i\ k) .2 \\ & \textsf{R}_i (\lang S,\rho \rang\ k) &&= \lang S,\textsf{R}_i \rho \rang (\textsf{R}_i\ k) \end{alignedat} $$ rbN 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.