Builds the vl-duperhs-alist-p for a list of assignments.
(vl-make-duperhs-alist x) → alist
Function:
(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:
(defthm vl-duperhs-alist-p-of-vl-make-duperhs-alist (b* ((alist (vl-make-duperhs-alist x))) (vl-duperhs-alist-p alist)) :rule-classes :rewrite)
Theorem:
(defthm vl-make-duperhs-alist-of-vl-assignlist-fix-x (equal (vl-make-duperhs-alist (vl-assignlist-fix x)) (vl-make-duperhs-alist x)))
Theorem:
(defthm vl-make-duperhs-alist-vl-assignlist-equiv-congruence-on-x (implies (vl-assignlist-equiv x x-equiv) (equal (vl-make-duperhs-alist x) (vl-make-duperhs-alist x-equiv))) :rule-classes :congruence)