The type of atoms is provided in order to model character strings. The canonical elements of the type atom are ``...'', where ... is any character string. Equality on atoms is decidable using the noncanonical form , which denotes s when and t otherwise.
Nuprl also provides the type of lists over any other type A; it is denoted . The canonical elements of the type are nil , which corresponds to the empty list, and , where a is in A and b is in . For example, the list of the first three positive integers in descending order is denoted .
It is customary in the theory of lists to have head and tail functions such that
andThese and all other functions on lists that are built inductively are defined in terms of the list induction form . The meaning of this form is given by the following equations.
With this form the tail function can be defined as . The basic definitions and facts from list theory appear in chapter 11.