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

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

    fn read_back_please(self) -> Self::NormalForm { ... }

    fn normal(
        index: u32, 
        me: Self, 
        other: Self
    ) -> (Self::NormalForm, Self::NormalForm) { ... }
}

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

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 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.

Loading content...

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]

impl ReadBack for CaseTree[src]

type NormalForm = NormalCaseTree

fn read_back_please(self) -> Self::NormalForm[src]

fn normal(
    index: u32,
    me: Self,
    other: Self
) -> (Self::NormalForm, Self::NormalForm)[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 normal(
    index: u32,
    me: Self,
    other: Self
) -> (Self::NormalForm, Self::NormalForm)[src]

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]

Loading content...