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.
