blob: 1def02cb270b3d1775a19d14eeb7e20bac3f49c3 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
last modified: Thu Dec 16 15:42:59 2004 by Eric Smith
This directory (bags/) contains the beginnings of an ACL2 library about bags (multisets). (This directory requires the following other directories (all created at Rockwell Collins): symbol-fns/ lists/ syntax/
.)
Typically, the user of this library should include bags/top. Users interested in "two-level" bags ("bags of bags") should consider including the books "two-level" and "two-level-meta".
The bags library is described in the 2004 ACL2 Workshop paper on bags by Smith, Nelesen, Greve, Wilding, and Richards.
So see:
http://www.cs.utexas.edu/users/moore/acl2/workshop-2004/
for more information and documentation on this library. See especially the "Future Work" section of the paper for TODOs for this library.
When this library is changed and improved it may get out of sync with the paper (which seems unlikely to be updated). Consider documenting such improvements in this file.
|
