Trait CoreFold

pub trait CoreFold<L: Language>: Sized + CoreVisit<L> {
    // Required method
    fn substitute(&self, substitution_fn: SubstitutionFn<'_, L>) -> Self;

    // Provided methods
    fn shift_in(&self) -> Self { ... }
    fn replace_free_var(
        &self,
        v: impl Upcast<CoreVariable<L>>,
        p: impl Upcast<CoreParameter<L>>,
    ) -> Self { ... }
}

Required Methods

fn substitute(&self, substitution_fn: SubstitutionFn<'_, L>) -> Self

Replace uses of variables with values from the substitution.

Provided Methods

fn shift_in(&self) -> Self

Produce a version of this term where any debruijn indices which appear free are incremented by one.

fn replace_free_var( &self, v: impl Upcast<CoreVariable<L>>, p: impl Upcast<CoreParameter<L>>, ) -> Self

Replace all appearances of free variable v with p.

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementations on Foreign Types

impl<L: Language> CoreFold<L> for u32

fn substitute(&self, _substitution_fn: SubstitutionFn<'_, L>) -> Self

impl<L: Language> CoreFold<L> for ()

fn substitute(&self, _substitution_fn: SubstitutionFn<'_, L>) -> Self

impl<L: Language> CoreFold<L> for usize

fn substitute(&self, _substitution_fn: SubstitutionFn<'_, L>) -> Self

impl<L: Language, A: CoreFold<L>, B: CoreFold<L>> CoreFold<L> for (A, B)

fn substitute(&self, substitution_fn: SubstitutionFn<'_, L>) -> Self

impl<L: Language, A: CoreFold<L>, B: CoreFold<L>, C: CoreFold<L>> CoreFold<L> for (A, B, C)

fn substitute(&self, substitution_fn: SubstitutionFn<'_, L>) -> Self

impl<L: Language, T: CoreFold<L>> CoreFold<L> for Option<T>

fn substitute(&self, substitution_fn: SubstitutionFn<'_, L>) -> Self

impl<L: Language, T: CoreFold<L>> CoreFold<L> for Arc<T>

fn substitute(&self, substitution_fn: SubstitutionFn<'_, L>) -> Self

impl<L: Language, T: CoreFold<L>> CoreFold<L> for Vec<T>

fn substitute(&self, substitution_fn: SubstitutionFn<'_, L>) -> Self

Implementors

impl<L: Language> CoreFold<L> for CoreSubstitution<L>

impl<L: Language, T: CoreFold<L> + Ord> CoreFold<L> for Set<T>

impl<L: Language, T: CoreFold<L>> CoreFold<L> for CoreBinder<L, T>