1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
|
((:files
"
.:
Makefile
alist-defthms.lisp
alist-defuns.lisp
alist-theory.lisp
array1.lisp
defalist.acl2
defalist.lisp
deflist.acl2
deflist.lisp
list-defthms.lisp
list-defuns.lisp
list-theory.lisp
no-duplicates.lisp
number-list-defthms.lisp
number-list-defuns.lisp
number-list-theory.lisp
set-defthms.lisp
set-defuns.lisp
set-theory.lisp
structures.acl2
structures.lisp
utilities.acl2
utilities.lisp
")
(:TITLE "Data structures")
(:AUTHOR/S
"Bill Bevier"
"Bishop Brock"
"Sol Swords"
"Others??"
)
(:KEYWORDS
"data structures"
"lists"
"alists"
"sets"
)
(:ABSTRACT "The books in this directory contain books for reasoning
about various data structures such as lists, alists, and sets.
Some of the books are documented in README, and others are not yet
documented. TODO: Copy the documentation from README into this
Readme.lsp file, and document the undocumented books.
no-duplicates.lisp: A simple but useful set of rewrite rules for
reasoning about NO-DUPLICATESP-EQUAL and INTERSECTP-EQUAL.
"))
|
