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.

Thu Sep 14 08:45:18 EDT 1995