Basic Types

The integers are a primitive type of Nuprl with primitive operations of Equality, in , and order, , are also primitive. The natural numbers are defined as , and the initial segments are . The segment and . So . Basic facts about these types can be found in these libraries: int_1, int_2, num_thy_1a.

Given any type , we can form the type of lists whose elements are all from . This is called . The empty list is denoted nil regardless of the type . The list_construction(or ``consing'') takes an element of and an , say , and forms a new list denoted . It adds the element from to the head of the list .

The append operation on lists is critical in this article; it is denoted and is defined in the usual recursive way

The Booleans, , consists of and denoting true and false. The normal if-then-else case selection is available along with the standard operations . We write the subscript ``b'' to distinguish these operations from the propositional connectives, , (see ).