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 fst(<x>) and snd(<x>) are the appropriate selector functions defined in terms of spread. If we made all the definitions involved in rational arithmetic in this manner then the size of the expanded form of an arithmetic expression could be exponentially larger than the displayed form. To avoid this we make better use of spread:
-<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 term_of(t), where t is a theorem name, instead of a combination of other definitions and Nuprl code. Here are a few examples.
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 mult_ might be
explicit intro
\x. \y. <fst(x)*fst(y), snd(x)*snd(y)>
where fst and snd are projections from pairs
defined using spread.
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 x@i:T -> x@i<x. The replacement, on the other hand,
results in all x:T. x<x; these two terms are not equal, so
the definition all is not retained and the display form of
the result is the former term.
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.