		Search-engine friendly clone of the ACL2 documentation.

Utilities

Clean-alist

Signature
(clean-alist x) → ans
Returns: ans — Type (alistp ans).

Definitions and Theorems

Function: clean-alist

(defun clean-alist (x)
  (declare (xargs :guard t))
  (let ((__function__ 'clean-alist))
    (declare (ignorable __function__))
    (b* ((fal (make-fal x nil))
         (shrink (hons-shrink-alist fal nil))
         (- (fast-alist-free fal))
         (- (fast-alist-free shrink)))
      shrink)))

Theorem: alistp-of-clean-alist

(defthm alistp-of-clean-alist
  (b* ((ans (clean-alist x)))
    (alistp ans))
  :rule-classes :rewrite)

Theorem: hons-assoc-equal-of-clean-alist

(defthm hons-assoc-equal-of-clean-alist
  (equal (hons-assoc-equal a (clean-alist x))
         (hons-assoc-equal a x)))