Function lamcal::substitute [−][src]
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.