Trait formality_core::fold::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.

Object Safety

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>