Function lamcal::substitute

pub fn substitute<A>(expr: &Term, var: &VarName, subst: &Term) -> Term where
    A: AlphaRename, 

Replaces all free occurrences of the variable var in the expression expr with the expression subst and returns the resulting expression.

This function implements substitution in terms of the lambda calculus as a recursion on the structure of the given expr.

The result is returned as a new Term. The original term expr is not changed.

To avoid name clashes this function performs α-conversions when appropriate. Therefore a strategy for α-conversion must be specified as the type parameter A.

This function returns the result as a new Term. The given term expr remains unmodified. If you want to substitute the original term in place use the associated function Term::subst instead.