Extraction Terms

Next: Appendix C: Direct Up: Simulating Lambda--prl Constructs Previous: Primitive Recursive Functions

To use the extracted term E from a (complete) theorem T in another theorem, make E a DEF:

         E==term_of(T).

The evaluation mechanism may be used to evaluate term_ of(T) and to bind its value to a variable.

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