Index of /users/moore/acl2/v3-4/distrib/acl2-sources/books/data-structures

 Name                    Last modified      Size  Description
 Parent Directory                             -   
 memories/               10-Aug-2008 15:07    -   
 Makefile                17-Dec-2007 09:59  2.1K  
 alist-defthms.lisp      17-Dec-2007 09:59   26K  
 alist-defuns.lisp       17-Dec-2007 09:59   18K  
 alist-theory.lisp       17-Dec-2007 09:59  1.0K  
 array1.lisp             17-Dec-2007 09:59   31K  
 certify.lsp             17-Dec-2007 09:59  1.7K  
 defalist.acl2           17-Dec-2007 09:59  114   
 defalist.lisp           17-Dec-2007 09:59   39K  
 define-structures-pa..> 17-Dec-2007 09:59  755   
 define-u-package.lisp   17-Dec-2007 09:59  1.0K  
 deflist.acl2            17-Dec-2007 09:59  113   
 deflist.lisp            17-Dec-2007 09:59   47K  
 list-defthms.lisp       17-Dec-2007 09:59   42K  
 list-defuns.lisp        13-Feb-2008 08:02  9.8K  
 list-theory.lisp        17-Dec-2007 09:59  1.0K  
 number-list-defthms...> 17-Dec-2007 09:59  3.1K  
 number-list-defuns.lisp 17-Dec-2007 09:59  5.2K  
 number-list-theory.lisp 17-Dec-2007 09:59  1.1K  
 set-defthms.lisp        17-Dec-2007 09:59  7.8K  
 set-defuns.lisp         17-Dec-2007 09:59  2.7K  
 set-theory.lisp         17-Dec-2007 09:59  1.0K  
 structures.acl2         17-Dec-2007 09:59  160   
 structures.lisp         17-Dec-2007 09:59   92K  
 utilities.acl2          17-Dec-2007 09:59  141   
 utilities.lisp          17-Dec-2007 09:59   37K  

The data-structures books provide definitions and rewrite rules about some of
the basic data structures frequently used in ACL2 and Common Lisp: lists,
alists, and structures.

The contents of each book are briefly documented below.

list-defuns         definitions of list functions
list-defthms        theorems about list functions
deflist             a tool for defining typed lists
list-theory         brings in all of the above

set-defuns          definitions of set functions
set-defthms         theorems about set functions
set-theory          brings in both the definitions and theorems

alist-defuns        definitions of alist functions
alist-defthms       theorems about alist functions
defalist            a tool for defining typed alists
alist-theory        brings in all of the above

number-list-defuns  definitions about lists of numbers
number-list-defthms theorems about number list functions
number-list-theory  brings on both the definitions and theorems

structures          a tool for defining typed record structures

The following books provide support for the above, but are not
themselves certified.  Users should not generally have any reason to
use these directly.

define-structures-package.lisp
define-u-package.lisp
utilities.lisp


Bill Bevier