Enum nar::syntax::core::subst::PrimSubst

pub enum PrimSubst<T> {
    IdS,
    Cons(T, Rc<Self>),
    Succ(Rc<Self>),
    Weak(DBI, Rc<Self>),
    Lift(DBI, Rc<Self>),
}

Substitution type. Agda.

Variants

IdS

The identity substitution. $$ \Gamma \vdash \text{IdS} : \Gamma $$

Cons(T, Rc<Self>)

The "add one more" substitution, or "substitution extension". $$ \cfrac{\Gamma \vdash u : A \rho \quad \Gamma \vdash \rho : \Delta} {\Gamma \vdash \text{Cons}(u, \rho) : \Delta, A} $$

Succ(Rc<Self>)

Strengthening substitution. Apply this to a term which does not contain variable 0 to lower all de Bruijn indices by one. $$ \cfrac{\Gamma \vdash \rho : \Delta} {\Gamma \vdash \text{Succ} \rho : \Delta, A} $$

Weak(DBI, Rc<Self>)

Weakening substitution, lifts to an extended context. $$ \cfrac{\Gamma \vdash \rho : \Delta} {\Gamma, \Psi \vdash \text{Weak}_\Psi \rho : \Delta} $$

Lift(DBI, Rc<Self>)

Lifting substitution. Use this to go under a binder. $\text{Lift}_1 \rho := \text{Cons}(\texttt{Term::form\_dbi(0)}, \text{Weak}_1 \rho)$. $$ \cfrac{\Gamma \vdash \rho : \Delta} {\Gamma, \Psi \rho \vdash \text{Lift}_\Psi \rho : \Delta, \Psi} $$

Methods

impl<T: DeBruijn> PrimSubst<T>

pub fn concat(ts: impl DoubleEndedIterator<Item = T>, to: Rc<Self>) -> Rc<Self>

Agda.

pub fn parallel(ts: impl DoubleEndedIterator<Item = T>) -> Rc<Self>

Agda.

pub fn cons(self: Rc<Self>, t: T) -> Rc<Self>

Agda.

impl<Term: DeBruijn + RedEx<Term, Term> + Clone> PrimSubst<Term>

pub fn lookup(&self, dbi: DBI) -> Term

pub fn raise_term(k: DBI, term: Term) -> Term

Agda.

pub fn raise_from(n: DBI, k: DBI, term: Term) -> Term

Agda.

pub fn compose(self: Rc<Self>, sgm: Rc<Self>) -> Rc<Self>

Agda.

pub fn lookup_impl(&self, dbi: DBI) -> Either<&Term, Term>

If lookup failed, return the DBI. Agda.

impl<T> PrimSubst<T>

pub fn raise(by: DBI) -> Rc<Self>

Agda.

pub fn drop_by(self: Rc<Self>, drop_by: DBI) -> Rc<Self>

Lift a substitution under k binders. Agda.

pub fn lift_by(self: Rc<Self>, lift_by: DBI) -> Rc<Self>

Lift a substitution under k binders. Agda.

pub fn weaken(self: Rc<Self>, weaken_by: DBI) -> Rc<Self>

Agda.

pub fn one(t: T) -> Rc<Self>

Trait Implementations

impl<T: Clone> Clone for PrimSubst<T>

fn clone(&self) -> PrimSubst<T>

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<T> Default for PrimSubst<T>

fn default() -> Self

Returns the "default value" for a type.