[−][src]Trait minitt::read_back::ReadBack

pub trait ReadBack: Sized {
    type NormalForm: Eq + Debug;
    fn read_back(self, index: u32) -> Self::NormalForm;

    fn eq_normal(self, index: u32, other: Self) -> Result<(), String> { ... }
}

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 :(

Loading content...

Required methods

fn read_back(self, index: u32) -> Self::NormalForm

Interface for rbV, rbN and rbRho in Mini-TT.

Loading content...

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.

Loading content...

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 Telescope<Name>[src]

type NormalForm = NormalTelescope<Name>

fn read_back(self, index: u32) -> Self::NormalForm[src]

rbRho in Mini-TT.

fn eq_normal(self, index: u32, other: Self) -> Result<(), String>[src]

Loading content...