top

(in-package "ACL2")

(defsection std/typed-lists
  :parents (std)
  :short "A library about the built-in typed lists, like @(see
character-listp), @(see nat-listp), @(see string-listp), etc."
  :long "<p>The @('std/typed-lists') library provides basic lemmas about
built-in ACL2 functions.</p>

<p>If you want to load everything in the library, you can just include the
@('top') book, e.g.,</p>

@({ (include-book "std/typed-lists/top" :dir :system) })

<p>Alternately, it is perfectly reasonable to just include the individual books
that deal with the typed lists you are interested in.  For instance,</p>

@({
    (include-book "std/typed-lists/character-listp" :dir :system)
    (include-book "std/typed-lists/symbol-listp" :dir :system)
    ;; and so on.
})

<p>Most of the typed-lists library is generated automatically by @(see
std::deflist).  You may find this macro useful for introducing your own, custom
typed lists.</p>")