A library about the built-in typed lists, like character-listp, nat-listp, string-listp, etc.
The std/typed-lists library provides basic lemmas about
built-in ACL2 functions.
If you want to load everything in the library, you can just include the
top book, e.g.,
(include-book "std/typed-lists/top" :dir :system)
Alternately, it is perfectly reasonable to just include the individual books
that deal with the typed lists you are interested in. For instance,
(include-book "std/typed-lists/character-listp" :dir :system)
(include-book "std/typed-lists/symbol-listp" :dir :system)
;; and so on.
Most of the typed-lists library is generated automatically by std::deflist. You may find this macro useful for introducing your own, custom
- Lemmas about character-listp available in the std/typed-lists library.
- Lemmas about symbol-listp available in the std/typed-lists library.
- Lemmas about boolean-listp available in the std/typed-lists library.
- Lemmas about string-listp available in the std/typed-lists library.
- Lemmas about eqlable-listp available in the std/typed-lists library.
- Theorems about true lists of true lists.
- Lemmas about atom-listp available in the std/typed-lists library.
- Recognizer for lists of unsigned-byte-p's.
- Like alistp but doesn't require that the final cdr is nil.
- (cons-list-listp x) recognizes lists where every element satisfies cons-listp.
- Recognizer for lists of signed-byte-p's.
- Recognize true lists of strings and symbols.