Nuprl's type theory is formulated in a sequent calculus
. The structure
of sequents is described in Section 
and of proofs
in Section
.
Both structures are defined in Lisp and are accessible from ML. For convenience, we use term-like notation to describe them, although they are not implemented or edited as terms. Perhaps they will be at some stage in the future.