next up previous contents index
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

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