Next: Equality and Propositions Up: Extending the Typed Previous: Integers

## Atoms and Lists

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

and
.
These 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.

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995