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.