next up previous contents index
Next: Appendix C: Direct Up: Simulating Lambda--prl Constructs Previous: Primitive Recursive Functions

Extraction Terms

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

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