| NuprlPrimitives | Explanations of Nuprl Primitives and Conventions |
| sqequal 1 | |
| list 1 | |
| int 2 | |
| fun 1 | |
| union | Non canonical functions (isl, outl, outr) for union type. |
| rel 1 | Common properties of binary relations. |
| bool 1 | |
| int 1 | |
| well fnd | |
| core | Some basic concepts defined type-theoretically. |