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
These and all other functions on lists that are built inductively are defined in terms of the list induction formand
.
.
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.
