pub trait Shift<I: Interner>: Fold<I> {
fn shifted_in(self, interner: I) -> Self::Result;
fn shifted_in_from(
self,
interner: I,
source_binder: DebruijnIndex
) -> Self::Result;
fn shifted_out(self, interner: I) -> Fallible<Self::Result>;
fn shifted_out_to(
self,
interner: I,
target_binder: DebruijnIndex
) -> Fallible<Self::Result>;
}
Expand description
Methods for converting debruijn indices to move values into or out of binders.
Required methods
fn shifted_in(self, interner: I) -> Self::Result
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
fn shifted_in_from(
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>
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>
fn shifted_out_to(
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.