Another large section of the library is the directory `lib_list`.
There are several files. The most basic is
`lib_list.l` which contains just the definition
of the inductive type list. The four files
`lib_list_Adjoin`, `lib_list_Distin`,
`lib_list_Member`, `lib_list_Perm` and `lib_list_PermII`
define the predicates Adjoin, Distin, Member and two version of Perm
respectively and prove theorems about them.
The other files in this directory are divided
according to their dependency on other
datatypes. The file `lib_list_basics`
contains functions and theorems which do not depend
on any other datatypes, `lib_list_bool` depends
on the boolean datatype. `lib_list_partial`
defines some properly partial functions using the sum
and empty datatypes to construct ``partial'' result types,
the ``length'' file defines functions dependent on
the natural number type, principally ``length'' but
also a couple of other functions. `lib_list_misc`
contains the one function
and theorem which require both sum and natural numbers.

- List Definitions
- List Basics
- List functions with booleans
- Partial List functions
- Length-like list functions
- Other list functions
- Lists and products
- The Relation Adjoin
- Membership
- Distinctness
- Permutation
- Sorted Lists