The advantages of the definition mechanism in are obvious, and it should be utilized as frequently as possible. By layering definitions finely, i.e., by having the right--hand sides of the definitions of theory objects mention primarily other definitions and not Nuprl code, the meaning will be clear at all stages of a proof. However, unless some care is taken it is easy to build definitions whose denoted text is very large, and this can affect system performance. In practice it has happened on occasion that objects whose display form looked quite innocent caused the system performance to be rather seriously degraded. Fortunately this problem can be avoided.

First, avoid unnecessary formal parameter duplication. For example, the obvious way to define negation of a rational number (which we think of as a pair of integers) is

-<x:Q> == < -fst(<x>), snd(<x>) >where

-<x:Q> == spread( <x>; u,v. <-u,v>).Of course, tricks such as the above cannot always be done, and even without formal parameter duplication defined objects will eventually be very large. A general way to handle the size buildup involves defining an object to be an extraction

THM Q_ >> U1 DEF Q Q == term_of(Q_) THM mult_ >> Q -> Q -> Q DEF mult <x:Q>*<y:Q> == term_of(mult_)(<x>)(<y>)Each of the two theorems would have an extraction which was the appropriate code. For example, the first step of the proof of

explicit intro \x. \y. <fst(x)*fst(y), snd(x)*snd(y)>where

This method of using extractions is workable because of
the direct computation rules .
When a variable is declared
in a hypothesis list to be of a type which is really an
extraction (such as the type ` Q` above), then the actual
(canonical) type must be obtained before an elimination of
the variable can be done. An application of the direct
computation rule will do this, and in fact it is easy
to incorporate such computations into tactics so that the
``indirectness'' of the definitions can be made virtually
invisible.

It might be useful to have an idea of when
display forms can be maintained. It is rather dismaying
to be proceeding smoothly through a proof and suddenly
come upon an unreadable chunk of raw Nuprl
code
resulting from definitions being eliminated. This
doesn't happen too often, but when it does it can make a
proof very difficult. Because definitions are
text macros (i.e., they are not tied to term structure), substitution
can cause definitions to be lost,
leaving only the actual text the definition references denote.
When a term **u** is substituted for a variable **x** in a term
**t**, two different kinds of replacement are done. First, the
usual substitution is done on the term **t**. Then a textual
replacement is done, with a result the same as would be
obtained by a user manually replacing in a ted window * all*
visible occurrences of **x**, whether free or bound. If the two
resulting terms are not equal (or if the textual replacement did not
even result in a term), then the definition is removed,
leaving just the term which resulted from the usual substitution.
For example, consider substituting ` x` for ` y`
in ` all x:T. x<y` (where ` all` has the usual definition).
The substitution requires --conversion; all ` x`'s in
the term are renamed ` x@ i`, and the substitution results
in

We end this section with a word about debugging definitions. Many of the basic objects of a theory have a computational meaning and so can be executed. Before one starts proving properties of these objects it is a good idea to ``debug'' them, i.e., to use the Nuprl evaluator to test the objects in order to remove trivial errors. In this way one can avoid the frustrating experience of reaching the bottom of a proof and discovering that it cannot be completed because of a mistake in one of the definitions used.

Thu Sep 14 08:45:18 EDT 1995