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
sourcefn shifted_in(self, interner: I) -> Self
fn shifted_in(self, interner: I) -> Self
Shifts this term in one level of binders.
sourcefn shifted_in_from(self, interner: I, source_binder: DebruijnIndex) -> Self
fn shifted_in_from(self, interner: I, source_binder: DebruijnIndex) -> Self
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.
sourcefn shifted_out(self, interner: I) -> Fallible<Self>
fn shifted_out(self, interner: I) -> Fallible<Self>
Shifts this term out one level of binders.
sourcefn shifted_out_to(
self,
interner: I,
target_binder: DebruijnIndex
) -> Fallible<Self>
fn shifted_out_to(
self,
interner: I,
target_binder: DebruijnIndex
) -> Fallible<Self>
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.