next up previous contents
Next: Arithmetic Operators Up: The Tactic Language Previous: The Special Theorems RAISE

The Special Theorems EVAL and BIND

These theorems implement abstraction and reduction for variable binding contexts: EVAL converts a term [?u] @ ?t by replacing the appropriate bound variable with t in u and ``demoting'' other bound variables as necessary. BIND @ ?t (note the parameter) applied to u converts it to the form [?U] @ ?t if the result [?U] of replacing each occurrence of t with the appropriate bound variable and ``promoting'' other bound variables as necessary is weakly stratified.

Randall Holmes
Fri Sep 5 16:28:58 MDT 1997