[−][src]Trait chalk_ir::fold::shift::Shift
Methods for converting debruijn indices to move values into or out of binders.
Required methods
fn shifted_in(&self, interner: &I) -> Self::Result
Shifts this term in one level of binders.
fn shifted_in_from(
&self,
interner: &I,
source_binder: DebruijnIndex
) -> Self::Result
&self,
interner: &I,
source_binder: DebruijnIndex
) -> Self::Result
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.
fn shifted_out(&self, interner: &I) -> Fallible<Self::Result>
Shifts this term out one level of binders.
fn shifted_out_to(
&self,
interner: &I,
target_binder: DebruijnIndex
) -> Fallible<Self::Result>
&self,
interner: &I,
target_binder: DebruijnIndex
) -> Fallible<Self::Result>
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
impl<T: Fold<I, I>, I: Interner> Shift<I> for T
[src]
fn shifted_in(&self, interner: &I) -> Self::Result
[src]
fn shifted_in_from(
&self,
interner: &I,
source_binder: DebruijnIndex
) -> T::Result
[src]
&self,
interner: &I,
source_binder: DebruijnIndex
) -> T::Result
fn shifted_out_to(
&self,
interner: &I,
target_binder: DebruijnIndex
) -> Fallible<T::Result>
[src]
&self,
interner: &I,
target_binder: DebruijnIndex
) -> Fallible<T::Result>