		Search-engine friendly clone of the ACL2 documentation.

Duperhs-check

Vl-make-duperhs-alist

Builds the vl-duperhs-alistp for a list of assignments.

Signature
(vl-make-duperhs-alist x) → alist
Arguments: x — Guard (vl-assignlist-p x).
Returns: alist — A slow alist.
Type (vl-duperhs-alistp alist), given the guard.

Definitions and Theorems

Function: vl-make-duperhs-alist

(defun vl-make-duperhs-alist (x)
  (declare (xargs :guard (vl-assignlist-p x)))
  (let ((__function__ 'vl-make-duperhs-alist))
    (declare (ignorable __function__))
    (b* ((alist (len x))
         (alist (vl-make-duperhs-alist-aux x alist))
         (ans (hons-shrink-alist alist nil)))
      (fast-alist-free alist)
      (fast-alist-free ans)
      ans)))

Theorem: vl-duperhs-alistp-of-vl-make-duperhs-alist

(defthm vl-duperhs-alistp-of-vl-make-duperhs-alist
  (implies (and (force (vl-assignlist-p x)))
           (b* ((alist (vl-make-duperhs-alist x)))
             (vl-duperhs-alistp alist)))
  :rule-classes :rewrite)