Type Definition minitt::syntax::TelescopeRaw

type TelescopeRaw = GenericTelescope<Value>;

Methods

impl TelescopeRaw

pub fn resolve(&self, name: &str) -> Result<Value, String>

getRho in Mini-TT.

Trait Implementations

impl<'_> ReadBack for &'_ TelescopeRaw

type NormalForm = NormalTelescope

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 read_back_please(self) -> Self::NormalForm

Sometimes you don't want to pass an argument, and let me do this for you :)

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

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