pub trait Shift<I: Interner>: TypeFoldable<I> {
    fn shifted_in(self, interner: I) -> Self;
    fn shifted_in_from(self, interner: I, source_binder: DebruijnIndex) -> Self;
    fn shifted_out(self, interner: I) -> Fallible<Self>;
    fn shifted_out_to(
        self,
        interner: I,
        target_binder: DebruijnIndex
    ) -> Fallible<Self>; }
Expand description

Methods for converting debruijn indices to move values into or out of binders.

Required methods

Shifts this term in one level of binders.

Shifts a term valid at outer_binder so that it is valid at the innermost binder. See DebruijnIndex::shifted_in_from for a detailed explanation.

Shifts this term out one level of binders.

Shifts a term valid at the innermost binder so that it is valid at outer_binder. See DebruijnIndex::shifted_out_to for a detailed explanation.

Implementors