[−][src]Trait minitt::check::read_back::ReadBack
Since all of Value
, Neutral
and Telescope
have a read back function,
I extracted this common interface for them.
Implementing Sized
to make the compiler happy.
Associated Types
type NormalForm: Eq + Display
Corresponding normal form type for the read-backable structures.
This is needed because Rust does not support Higher-Kinded Types :(
Required methods
fn read_back(self, index: u32) -> Self::NormalForm
Interface for rbV
, rbN
and rbRho
in Mini-TT.
Provided methods
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)
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.
Implementors
impl ReadBack for Value
[src]
type NormalForm = NormalExpression
fn read_back(self, index: u32) -> Self::NormalForm
[src]
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 ReadBack for CaseTree
[src]
type NormalForm = NormalCaseTree
fn read_back(self, index: u32) -> Self::NormalForm
[src]
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 ReadBack for Neutral
[src]
type NormalForm = NormalNeutral
fn read_back(self, index: u32) -> Self::NormalForm
[src]
rbN
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<'_> ReadBack for &'_ TelescopeRaw
[src]
type NormalForm = NormalTelescope
fn read_back(self, index: u32) -> Self::NormalForm
[src]
rbRho
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)