Function lamcal::apply

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);