		Search-engine friendly clone of the ACL2 documentation.

Basic-bind-elim

Vl-bindintentlist->modinsts

Signature
(vl-bindintentlist->modinsts x) → insts
Arguments: x — Guard (vl-bindintentlist-p x).
Returns: insts — Type (vl-modinstlist-p insts).

Definitions and Theorems

Function: vl-bindintentlist->modinsts

(defun vl-bindintentlist->modinsts (x)
  (declare (xargs :guard (vl-bindintentlist-p x)))
  (let ((__function__ 'vl-bindintentlist->modinsts))
    (declare (ignorable __function__))
    (if (atom x)
        nil
      (append (vl-bindintent->modinsts (car x))
              (vl-bindintentlist->modinsts (cdr x))))))

Theorem: vl-modinstlist-p-of-vl-bindintentlist->modinsts

(defthm vl-modinstlist-p-of-vl-bindintentlist->modinsts
  (b* ((insts (vl-bindintentlist->modinsts x)))
    (vl-modinstlist-p insts))
  :rule-classes :rewrite)

Theorem: vl-bindintentlist->modinsts-of-vl-bindintentlist-fix-x

(defthm vl-bindintentlist->modinsts-of-vl-bindintentlist-fix-x
  (equal (vl-bindintentlist->modinsts (vl-bindintentlist-fix x))
         (vl-bindintentlist->modinsts x)))

Theorem: vl-bindintentlist->modinsts-vl-bindintentlist-equiv-congruence-on-x

(defthm
 vl-bindintentlist->modinsts-vl-bindintentlist-equiv-congruence-on-x
 (implies (vl-bindintentlist-equiv x x-equiv)
          (equal (vl-bindintentlist->modinsts x)
                 (vl-bindintentlist->modinsts x-equiv)))
 :rule-classes :congruence)