		Search-engine friendly clone of the ACL2 documentation.

Dupeinst-check

Vl-make-dupeinst-alist

Builds a (slow) vl-dupeinst-alistp for a list of assignments.

Signature
(vl-make-dupeinst-alist x) → alist
Arguments: x — Guard (vl-modinstlist-p x).
Returns: alist — Type (vl-dupeinst-alistp alist), given the guard.

Definitions and Theorems

Function: vl-make-dupeinst-alist

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

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

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

Subtopics

Vl-make-dupeinst-alist-aux