The EVAL mechanism may be run interactively by typing the command
` eval` in the command window.
This command replaces the ` P>` prompt with the ` E>` prompt.
Two kinds of expressions may be entered after this prompt: Nuprl
terms and bindings.
Every expression must be terminated by ` ;;` and may extend for any
number of lines.
Entering a term results in that term being evaluated and its value
being displayed.
A binding has the form ` let id = term`.
Entering a binding results in the evaluation of the term
and the resulting value being bound
to

For example, suppose we have a theorem named ` bruce` with main goal

>> x:int -> y:int # (x=y in int)proved so that the extracted term is

... ... |P>eval | |E>let p1 = \x.spread(x;u,v.u);; | |\x.spread(x;u,v.u) | |E>let t = term_of(bruce);; | |\x.<x,axiom> | |E>t(17);; | |<17,axiom> | |E>p1(t(17));; | |17 | ... ...

The Nuprl
command ` create name eval place` creates a library
object that can contain any number of bindings (all terminated by

**Figure:** The Noncanonical Forms

Thu Sep 14 08:45:18 EDT 1995