next up previous contents index
Next: Unification Up: Tools for Tactic Previous: Tacticals

Substitution

Two functions currently perform substitutions  in terms: substitute and replace. Both take a term and a substitution as arguments and produce a term, where a substitution is a list of pairs, the first element of which is a term representing the variable to be substituted for and the second element of which is the term to substitute for that variable. The function substitute will automatically rename bound variables in order to avoid capture in the term during the substitution,gif while the function replace will perform a substitution without regard to capture.



Richard Eaton
Thu Sep 14 08:45:18 EDT 1995