Using the Evaluator

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 id in the EVAL environment and this value being displayed. The EVAL environment persists from one invocation of eval to the next. An EVAL session is terminated by .

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

        >> x:int -> y:int # (x=y in int)

x.<x,axiom>

...
...
|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 ;;). The library objects created in this way are edited using ted and so may contain def refs. Checking an EVAL object augments the EVAL environment by evaluating the bindings it contains. All EVAL objects in a library are evaluated when the library is loaded.

  
Figure: The Noncanonical Forms