next up previous contents index
Next: Programming Modes Up: Components of the Previous: Proof Editing


The evaluation mechanism allows us to regard as a functional  programming language. For example, the multiplication function in Nuprl notation is x. y.(x*y), and one can evaluate ( x. y.(x*y))(2)(3) to obtain the value 6. Of course, one can define much more complex data such as infinite precision real numbers and functions on them such as multiplication (see section 11.6). In this case we might also evaluate the form ( x. y.mult(x,y))(e)(pi)(50), which might print the first 50 digits of the infinite precision multiplication of the transcendental numbers e and .

The evaluation mechanism can also use a special form, term_of(t) , where t is a theorem. The term_of operation extracts the constructive meaning of a theorem. Thus if we have proved a theorem named t of the form for all x of type A there is a y of type B such that then term_of(t) extracts  a function mapping any a in A to a pair consisting of an element from B, say b, and a proof, say p, of . By selecting the first element of this pair we can build a function f from A to B such that for all x in A. The system also provides a mechanism for naming and storing executable terms in the library.

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