A number of other logical concepts can be expressed in Nuprl. For example,
the * conditional and* is sometimes used when
dealing with partial
functions. This connective can be defined as
` <p:prop> cand <q:prop> == (x:<p> # <q>)`. This
results in an and connective which forces the
evaluation of its first argument before the second argument.

As another example, sometimes it is useful to simplify the structure of a type considered as a proposition by ``squashing'' all of the proofs into one object. This squash operator is defined as

|| <p:prop> || == {0 in int | <p> }.Thus if

Thu Sep 14 08:45:18 EDT 1995