[−][src]Trait minitt::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 eq_normal(self, index: u32, other: Self) -> Result<(), String>
eqNf
in Mini-TT.
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 eq_normal(self, index: u32, other: Self) -> Result<(), String>
[src]
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 eq_normal(self, index: u32, other: Self) -> Result<(), String>
[src]
impl<'_> ReadBack for &'_ TelescopeRaw
[src]
type NormalForm = NormalTelescope
fn read_back(self, index: u32) -> Self::NormalForm
[src]
rbRho
in Mini-TT.