		Search-engine friendly clone of the ACL2 documentation.

Unparameterization

Vl-genblob-split-scopeitems

Signature
(vl-genblob-split-scopeitems x) → (mv scopeitems nonscopeitems)
Arguments: x — Guard (vl-genblob-p x).
Returns: scopeitems — Type (vl-genblob-p scopeitems).; nonscopeitems — Type (vl-genblob-p nonscopeitems).

Definitions and Theorems

Function: vl-genblob-split-scopeitems

(defun vl-genblob-split-scopeitems (x)
  (declare (xargs :guard (vl-genblob-p x)))
  (let ((__function__ 'vl-genblob-split-scopeitems))
    (declare (ignorable __function__))
    (b* (((vl-genblob x)))
      (mv (make-vl-genblob :portdecls x.portdecls
                           :vardecls x.vardecls
                           :paramdecls x.paramdecls
                           :fundecls x.fundecls
                           :taskdecls x.taskdecls
                           :modinsts x.modinsts
                           :gateinsts x.gateinsts
                           :typedefs x.typedefs
                           :imports x.imports
                           :fwdtypedefs x.fwdtypedefs
                           :modports x.modports
                           :genvars x.genvars
                           :generates x.generates
                           :ports x.ports
                           :scopetype x.scopetype
                           :id x.id)
          (change-vl-genblob x
                             :portdecls nil
                             :vardecls nil
                             :paramdecls nil
                             :fundecls nil
                             :taskdecls nil
                             :modinsts nil
                             :gateinsts nil
                             :typedefs nil
                             :fwdtypedefs nil
                             :modports nil
                             :genvars nil
                             :generates nil
                             :ports nil)))))

Theorem: vl-genblob-p-of-vl-genblob-split-scopeitems.scopeitems

(defthm vl-genblob-p-of-vl-genblob-split-scopeitems.scopeitems
  (b* (((mv ?scopeitems ?nonscopeitems)
        (vl-genblob-split-scopeitems x)))
    (vl-genblob-p scopeitems))
  :rule-classes :rewrite)

Theorem: vl-genblob-p-of-vl-genblob-split-scopeitems.nonscopeitems

(defthm vl-genblob-p-of-vl-genblob-split-scopeitems.nonscopeitems
  (b* (((mv ?scopeitems ?nonscopeitems)
        (vl-genblob-split-scopeitems x)))
    (vl-genblob-p nonscopeitems))
  :rule-classes :rewrite)

Theorem: vl-genblob-split-scopeitems-of-vl-genblob-fix-x

(defthm vl-genblob-split-scopeitems-of-vl-genblob-fix-x
  (equal (vl-genblob-split-scopeitems (vl-genblob-fix x))
         (vl-genblob-split-scopeitems x)))

Theorem: vl-genblob-split-scopeitems-vl-genblob-equiv-congruence-on-x

(defthm vl-genblob-split-scopeitems-vl-genblob-equiv-congruence-on-x
  (implies (vl-genblob-equiv x x-equiv)
           (equal (vl-genblob-split-scopeitems x)
                  (vl-genblob-split-scopeitems x-equiv)))
  :rule-classes :congruence)