# Deflist

Define a list type with a fixing function, supported by deftypes.

Deflist provides a recognizer predicate, fixing function, and
a few theorems defining a list of elements of a certain type.

Deflist is compatible with deftypes, and can be
mutually-recursive with other deftypes compatible type generators. As
with all deftypes-compatible type generators, its element type must
either be one produced by a compatible type generator or else have an
associated fixing function given by deffixtype. See basetypes for
some base types with fixing functions.

The syntax of deflist is:

(deflist foolist
:elt-type foo ;; required, must have a known fixing function
:parents (...) ;; xdoc
:short "..." ;; xdoc
:long "..." ;; xdoc
:measure (+ 1 (* 2 (acl2-count x)))
;; default: (acl2-count x)
:xvar x ;; default: x, or find x symbol in measure
:prepwork ;; admit these events before starting
:pred foolistp ;; default: foolist-p
:fix foolistfix ;; default: foolist-fix
:equiv foolist-= ;; default: foolist-equiv
:count foolistcnt ;; default: foolist-count
;; (may be nil; skipped unless mutually recursive)
:no-count t ;; default: nil, same as :count nil
:true-listp t ;; default: nil, require nil final cdr
:elementp-of-nil ;; default: :unknown, where nil has type foo or not
)

Only the name and the :elt-type argument is required.

As part of the event, deflist calls std::deflist to produce
several useful theorems about the introduced predicate.

Deflist (by itself, not when part of mutually-recursive deftypes form)
also allows previously defined list predicates. For example, the following
form produces a fixing function for ACL2's built-in string-listp
predicate:

(deflist string-list :pred string-listp :elt-type stringp)

If the predicate has been previously defined by `std::deflist`, then
the :true-listp and :elementp-of-nil values of the fty::deflist
must be the same as the ones of the `std::deflist`. Otherwise, the
fty::deflist may attempt to generate some theorems that have the same name
as, but slightly different formulas from, theorems generated by the `std::deflist`, causing an error.

The theorems generated by deflist depend on the currently included
books. For instance, if std/lists/sets.lisp is included, certain theorems
involving `member` are generated. This provides more modularity, by not
automatically including something like std/lists/top.lisp with
deflist. If deflist is called again with the same argument after
including more books, additional theorems corresponding to the newly included
books may be generated. See also the `Pluggable Architecture' section of
`std::deflist`.

### Subtopics

- Deflist-of-len
- Introduce a fixtype of
lists of a specified length.