Function lamcal::apply [−][src]
pub fn apply<A>(expr: &Term, subst: &Term) -> Term where
A: AlphaRename,
Applies a given lambda abstraction to the given substitution term and
returns the result as a new Term
.
If the given term expr
is a lambda abstraction (that is of variant
Term::Lam
) any occurrence of its bound variable in its body is replaced by
the given term subst
. The substitution is applied recursively.
The result is returned as a new Term
. The original term expr
is not
changed. If the given expression expr
is not a lambda abstraction an
unmodified clone of the term expr
is returned.
To avoid name clashes this function performs α-conversions when appropriate.
Therefore a strategy for α-conversion must be specified as a type parameter
A
.
This function returns the result as a new Term
. The given term expr
remains unmodified. If you want to apply an α-conversion on the original
term in place use the associated function
Term::apply
instead.
Examples
In the first example a lambda abstraction is applied to a variable z:
let expr1 = lam("x", app(var("x"), var("y"))); let expr2 = apply::<Enumerate>(&expr1, &var("z")); assert_eq!(expr2, app(var("z"), var("y")));
In this example a function application is applied to the variable z. Due to an application can not be applied to a variable, the returned expression is the same as the input expression:
let expr1 = app(var("x"), var("y")); let expr2 = apply::<Enumerate>(&expr1, &var("z")); assert_eq!(expr2, expr1);