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

 Name                    Last modified      Size  Description
 Parent Directory                             -   
 memories/               29-May-2006 00:06    -   
 Makefile                05-Mar-2005 17:24  2.1K  
 alist-defthms.lisp      18-Jun-2001 13:55   26K  
 alist-defuns.lisp       19-May-1997 12:18   18K  
 alist-theory.lisp       19-May-1997 12:18  1.0K  
 array1.lisp             20-May-1998 21:02   28K  
 certify.lsp             01-Jan-2001 22:34  1.7K  
 defalist.acl2           03-Dec-1998 14:19  114   
 defalist.lisp           08-Nov-2001 08:06   39K  
 define-structures-pa..> 04-Jun-2000 23:06  755   
 define-u-package.lisp   19-May-1997 12:19  1.0K  
 deflist.acl2            03-Dec-1998 14:19  113   
 deflist.lisp            17-Jul-2005 13:17   47K  
 list-defthms.lisp       21-Aug-2001 11:14   42K  
 list-defuns.lisp        23-Apr-2004 10:53  9.6K  
 list-theory.lisp        19-May-1997 12:19  1.0K  
 number-list-defthms...> 07-May-2000 09:48  3.1K  
 number-list-defuns.lisp 07-May-2000 09:44  5.2K  
 number-list-theory.lisp 19-May-1997 12:20  1.1K  
 set-defthms.lisp        19-May-1997 12:20  7.8K  
 set-defuns.lisp         19-May-1997 12:20  2.7K  
 set-theory.lisp         19-May-1997 12:21  1.0K  
 structures.acl2         03-Dec-1998 14:19  160   
 structures.lisp         18-Jan-2004 15:02   92K  
 utilities.acl2          03-Dec-1998 14:19  141   
 utilities.lisp          17-Jul-2005 13:18   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