|
|
|---|
|
|
|
|---|
Apply a substitution to an expression.
(subst-expression subst expr) → new-expr
Literals are unchanged.
If a variable is in the substitution map, we replace it with its associated expression. Otherwise the variable is unchanged.
Most expressions and related entities (e.g. branches) are transformed by recursively applying the substitution to subexpressions.
When we encounter a binding, we remove from the substitution map the bound variables before applying the (new) substitution to the body.