# 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.