[−][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 + Debug
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 eq_normal(self, index: u32, other: Self) -> Result<(), String>
eqNf
in Mini-TT.
Whether two structures are equivalent up to normal form.
Implementors
impl<Name: DebuggableNameTrait> ReadBack for Value<Name>
[src]
type NormalForm = NormalExpression<Name>
fn read_back(self, index: u32) -> Self::NormalForm
[src]
rbV
in Mini-TT.
fn eq_normal(self, index: u32, other: Self) -> Result<(), String>
[src]
impl<Name: DebuggableNameTrait> ReadBack for Neutral<Name>
[src]
type NormalForm = NormalNeutral<Name>
fn read_back(self, index: u32) -> Self::NormalForm
[src]
rbN
in Mini-TT.
fn eq_normal(self, index: u32, other: Self) -> Result<(), String>
[src]
impl<Name: DebuggableNameTrait, '_> ReadBack for &'_ TelescopeRaw<Name>
[src]
type NormalForm = NormalTelescope<Name>
fn read_back(self, index: u32) -> Self::NormalForm
[src]
rbRho
in Mini-TT.