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

Icon  Name                    Last modified      Size  Description
[DIR] Parent Directory                             -   
[DIR] memories/               01-May-2009 11:09    -   
[   ] Makefile                13-Oct-2008 14:03   50   
[TXT] alist-defthms.lisp      13-Oct-2008 14:03   26K  
[TXT] alist-defuns.lisp       13-Oct-2008 14:03   18K  
[TXT] alist-theory.lisp       13-Oct-2008 14:03  1.0K  
[TXT] array1.lisp             13-Oct-2008 14:03   31K  
[   ] defalist.acl2           13-Oct-2008 14:03  113   
[TXT] defalist.lisp           13-Oct-2008 14:03   39K  
[   ] define-structures-pa..> 13-Oct-2008 14:03  755   
[TXT] define-u-package.lsp    13-Oct-2008 14:03  1.0K  
[   ] deflist.acl2            13-Oct-2008 14:03  112   
[TXT] deflist.lisp            13-Oct-2008 14:03   47K  
[TXT] list-defthms.lisp       10-Dec-2008 09:22   42K  
[TXT] list-defuns.lisp        13-Oct-2008 14:03  9.8K  
[TXT] list-theory.lisp        13-Oct-2008 14:03  1.0K  
[TXT] number-list-defthms...> 13-Oct-2008 14:03  3.1K  
[TXT] number-list-defuns.lisp 13-Oct-2008 14:03  5.2K  
[TXT] number-list-theory.lisp 13-Oct-2008 14:03  1.1K  
[TXT] set-defthms.lisp        13-Oct-2008 14:03  7.8K  
[TXT] set-defuns.lisp         13-Oct-2008 14:03  2.7K  
[TXT] set-theory.lisp         13-Oct-2008 14:03  1.0K  
[   ] structures.acl2         13-Oct-2008 14:03  158   
[TXT] structures.lisp         13-Oct-2008 14:03   92K  
[   ] utilities.acl2          13-Oct-2008 14:03  140   
[TXT] utilities.lisp          13-Oct-2008 14:03   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.lsp
define-u-package.lsp
utilities.lisp


Bill Bevier