Type Definition minitt::syntax::Telescope

type Telescope<Name> = GenericTelescope<Name, Value<Name>>;

Rho in Mini-TT, dependent context.

Methods

impl<Name: DebuggableNameTrait> Telescope<Name>

pub fn resolve(&self, name: &Name) -> Value<Name>

getRho in Mini-TT.

Trait Implementations

impl<Name: DebuggableNameTrait> ReadBack for Telescope<Name>

type NormalForm = NormalTelescope<Name>

Corresponding normal form type for the read-backable structures. This is needed because Rust does not support Higher-Kinded Types :(

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

rbRho in Mini-TT.

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

eqNf in Mini-TT. Whether two structures are equivalent up to normal form.