next up previous contents
Next: List Definitions Up: The LEGO library - Previous: Exponentiation


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.