Std/typed-lists
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
typed lists.
Subtopics
- Std/typed-lists/character-listp
- Lemmas about character-listp available in the std/typed-lists library.
- Std/typed-lists/symbol-listp
- Lemmas about symbol-listp available in the std/typed-lists library.
- Std/typed-lists/boolean-listp
- Lemmas about boolean-listp available in the std/typed-lists library.
- Std/typed-lists/string-listp
- Lemmas about string-listp available in the std/typed-lists library.
- Std/typed-lists/eqlable-listp
- Lemmas about eqlable-listp available in the std/typed-lists library.
- Theorems-about-true-list-lists
- Theorems about true lists of true lists.
- Std/typed-lists/atom-listp
- Lemmas about atom-listp available in the std/typed-lists library.
- Unsigned-byte-listp
- Recognizer for lists of unsigned-byte-p's.
- Cons-listp
- Like alistp but doesn't require that the final cdr is nil.
- Cons-list-listp
- (cons-list-listp x) recognizes lists where every element satisfies cons-listp.
- Signed-byte-listp
- Recognizer for lists of signed-byte-p's.
- String-or-symbol-listp
- Recognize true lists of strings and symbols.
