		Search-engine friendly clone of the ACL2 documentation.

Vl-description

Vl-make-descalist

Signature
(vl-make-descalist x) → alist
Arguments: x — Guard (vl-descriptionlist-p x).
Returns: alist — Type (vl-descalist-p alist).

Definitions and Theorems

Function: vl-make-descalist

(defun vl-make-descalist (x)
  (declare (xargs :guard (vl-descriptionlist-p x)))
  (let ((__function__ 'vl-make-descalist))
    (declare (ignorable __function__))
    (b* (((when (atom x)) nil)
         (x1 (vl-description-fix (car x)))
         (name1 (vl-description->name x1))
         ((unless name1)
          (vl-make-descalist (cdr x))))
      (hons-acons name1 x1 (vl-make-descalist (cdr x))))))

Theorem: vl-descalist-p-of-vl-make-descalist

(defthm vl-descalist-p-of-vl-make-descalist
  (b* ((alist (vl-make-descalist x)))
    (vl-descalist-p alist))
  :rule-classes :rewrite)

Theorem: vl-make-descalist-of-vl-descriptionlist-fix-x

(defthm vl-make-descalist-of-vl-descriptionlist-fix-x
  (equal (vl-make-descalist (vl-descriptionlist-fix x))
         (vl-make-descalist x)))

Theorem: vl-make-descalist-vl-descriptionlist-equiv-congruence-on-x

(defthm vl-make-descalist-vl-descriptionlist-equiv-congruence-on-x
  (implies (vl-descriptionlist-equiv x x-equiv)
           (equal (vl-make-descalist x)
                  (vl-make-descalist x-equiv)))
  :rule-classes :congruence)