Std
Standard libraries for ACL2.
The std library is meant to become ACL2, Batteries
Included. Its features a wide variety of books that work well together to
provide a well-thought-out, documented, coherent reasoning strategy.
Std is currently under active development. You are welcome to use it,
but please be aware that things may change out from under you.
So far, std itself includes libraries about
basic concepts,
lists,
sets,
alists,
typed-lists,
stobjs,
input/output.
Each of these libraries provides many lemmas for reasoning about built-in
ACL2 functions, and also many additional functions. There is also a very
convenient std/util macro library, with macros that automate many
otherwise-tedious tasks. There is also a std/testing library with
utilities to create tests.
Subtopics
- Std/lists
- A library for reasoning about basic list operations like append, len, member, take, etc.
- Std/alists
- A library for reasoning about association list (alist) operations
like alist-keys, alist-vals, hons-get, etc.
- Obags
- A library of obags (ordered bags),
i.e. finite bags (a.k.a. multisets)
represented as non-strictly ordered lists.
- Std/util
- A macro library that automates defining types, introducing typed
functions, mapping over lists, and many other boilerplate tasks.
- Std/strings
- A library with many useful functions for working with strings, and
for reasoning about ACL2's built-in string operations and these new
operations.
- Std/io
- A library for reasoning about file input/output operations.
- Std/osets
- A finite set theory implementation for ACL2 based on fully ordered
lists. Some major features of this approach are that set equality is just
equal, and set operations like union, intersect, and so
forth have O(n) implementations.
- Std/basic
- A collection of very basic functions that are occasionally
convenient.
- Std/system
- A library that complements the built-in system utilities with theorems and with non-built-in system utilities.
- Std/typed-lists
- A library about the built-in typed lists, like character-listp, nat-listp, string-listp, etc.
- Std/bitsets
- Optimized libraries for representing finite sets of natural numbers
using bit masks, featuring a strong connection to the std/osets library.
- Std/testing
- A library of testing utilities.
- Std/typed-alists
- Typed alists.
- Std/stobjs
- A library for working with stobjs.
