Define an alist type with a fixing function, supported by deftypes.
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.
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
(defalist timer-alist :pred timer-alistp :key-type symbolp :val-type rational-listp)
Similarly to deflist, the theorems generated by