[−][src]Type Definition minitt::syntax::Telescope
type Telescope<Name> = GenericTelescope<Name, Value<Name>>;
Rho
in Mini-TT, dependent context.
Methods
impl<Name: DebuggableNameTrait> Telescope<Name>
[src]
Trait Implementations
impl<Name: DebuggableNameTrait> ReadBack for Telescope<Name>
[src]
type NormalForm = NormalTelescope<Name>
Corresponding normal form type for the read-backable structures. This is needed because Rust does not support Higher-Kinded Types :( Read more
fn read_back(self, index: u32) -> Self::NormalForm
[src]
rbRho
in Mini-TT.
fn eq_normal(self, index: u32, other: Self) -> Result<(), String>
[src]
eqNf
in Mini-TT. Whether two structures are equivalent up to normal form. Read more