Canonical Forms - continued from Computation

First, we list those operators that happen to be used to denote type constructors, although so classifying operators is not part of how they evaluate.

x:AB(x)
u:AB(u)
Type{i}	(where i is a Level Expression)
Atom
Void
a<b
A+B
u,v:A//E(u;v)
{x:A| B(x) }
u = v  A
x:A. B(x)
A List
rec(A.F(A))
a ~ b

Here are the remainder of the canonical forms:

*
inl(a)
inr(b)
nil
a.as
<a,b>
x.b(x)
"$tok"	(where $tok is a string of characters)
$n	(where $n is one or more digits)

See NonCanonical Forms.

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html