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.