		Search-engine friendly clone of the ACL2 documentation.

Defalist

Define an alist type with a fixing function, supported by deftypes.

Defalist provides a recognizer predicate, fixing function, and a few theorems defining an alist with keys of some type mapping to values of some type.

Defalist is compatible with deftypes, and can be mutually-recursive with other deftypes compatible type generators. As with all deftypes-compatible type generators, its key and value types must either be one produced by a compatible type generator or else have an associated fixing function given by deffixtype. (They may also be untyped.) See basetypes for some base types with fixing functions.

The syntax of defalist is:

(defalist fooalist
  :key-type symbol
  :val-type foo
  :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 fooalistp     ;; default: fooalist-p
  :fix fooalistfix    ;; default: fooalist-fix
  :equiv fooalist-=   ;; default: fooalist-equiv
  :count fooalistcnt  ;; default: fooalist-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
  :strategy :drop-keys ;; default: :fix-keys
)

The keyword arguments are all optional, although it doesn't make much sense to define an alist with neither a key-type nor value-type.

The :strategy keyword changes the way the fixing function works; by default, every pair in the alist is kept but its key and value are fixed. With :strategy :drop-keys, pairs with malformed keys are dropped, but malformed values are still fixed. Defmap is an abbreviation for defalist with :strategy :drop-keys.

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

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

(defalist timer-alist :pred timer-alistp
                      :key-type symbolp
                      :val-type rational-listp)

Similarly to deflist, the theorems generated by defalist depend on the currently included books, and calling defalist again with the same argument after including more books may generate additional theorem. See deflist for more details.