		Search-engine friendly clone of the ACL2 documentation.

Wildelim

Vl-design-wildelim

Top-level wildelim transform.

Signature
(vl-design-wildelim x) → new-x
Arguments: x — Guard (vl-design-p x).
Returns: new-x — Type (vl-design-p new-x).

Definitions and Theorems

Function: vl-design-wildelim

(defun vl-design-wildelim (x)
  (declare (xargs :guard (vl-design-p x)))
  (let ((__function__ 'vl-design-wildelim))
    (declare (ignorable __function__))
    (b* (((vl-design x) x))
      (change-vl-design x
                        :mods (vl-modulelist-wildelim x.mods)))))

Theorem: vl-design-p-of-vl-design-wildelim

(defthm vl-design-p-of-vl-design-wildelim
  (b* ((new-x (vl-design-wildelim x)))
    (vl-design-p new-x))
  :rule-classes :rewrite)

Theorem: vl-design-wildelim-of-vl-design-fix-x

(defthm vl-design-wildelim-of-vl-design-fix-x
  (equal (vl-design-wildelim (vl-design-fix x))
         (vl-design-wildelim x)))

Theorem: vl-design-wildelim-vl-design-equiv-congruence-on-x

(defthm vl-design-wildelim-vl-design-equiv-congruence-on-x
  (implies (vl-design-equiv x x-equiv)
           (equal (vl-design-wildelim x)
                  (vl-design-wildelim x-equiv)))
  :rule-classes :congruence)

Subtopics

Vl-modulelist-wildelim: (vl-modulelist-wildelim x) maps vl-module-wildelim across a list.
Vl-packeddimensionlist-wildelim: Eliminate ==? and !=? operators throughout a vl-packeddimensionlist-p.
Vl-namedparamvaluelist-wildelim: Eliminate ==? and !=? operators throughout a vl-namedparamvaluelist-p.
Vl-paramvaluelist-wildelim: Eliminate ==? and !=? operators throughout a vl-paramvaluelist-p.
Vl-plainarglist-wildelim: Eliminate ==? and !=? operators throughout a vl-plainarglist-p.
Vl-namedarglist-wildelim: Eliminate ==? and !=? operators throughout a vl-namedarglist-p.
Vl-maybe-delayoreventcontrol-wildelim: Eliminate ==? and !=? operators throughout a vl-maybe-delayoreventcontrol-p
Vl-enumitemlist-wildelim: Eliminate ==? and !=? operators throughout a vl-enumitemlist-p.
Vl-evatomlist-wildelim: Eliminate ==? and !=? operators throughout a vl-evatomlist-p.
Vl-rangelist-wildelim: Eliminate ==? and !=? operators throughout a vl-rangelist-p.
Vl-maybe-packeddimension-wildelim: Eliminate ==? and !=? operators throughout a vl-maybe-packeddimension-p
Vl-repeateventcontrol-wildelim: Eliminate ==? and !=? operators throughout a vl-repeateventcontrol-p
Vl-paramtype-wildelim: Eliminate ==? and !=? operators throughout a vl-paramtype-p
Vl-delayoreventcontrol-wildelim: Eliminate ==? and !=? operators throughout a vl-delayoreventcontrol-p
Vl-packeddimension-wildelim: Eliminate ==? and !=? operators throughout a vl-packeddimension-p
Vl-maybe-paramvalue-wildelim: Eliminate ==? and !=? operators throughout a vl-maybe-paramvalue-p
Vl-namedparamvalue-wildelim: Eliminate ==? and !=? operators throughout a vl-namedparamvalue-p
Vl-maybe-gatedelay-wildelim: Eliminate ==? and !=? operators throughout a vl-maybe-gatedelay-p
Vl-maybe-datatype-wildelim: Eliminate ==? and !=? operators throughout a vl-maybe-datatype-p
Vl-paramdecllist-wildelim: Eliminate ==? and !=? operators throughout a vl-paramdecllist-p.
Vl-portdecllist-wildelim: Eliminate ==? and !=? operators throughout a vl-portdecllist-p.
Vl-paramargs-wildelim: Eliminate ==? and !=? operators throughout a vl-paramargs-p
Vl-maybe-range-wildelim: Eliminate ==? and !=? operators throughout a vl-maybe-range-p
Vl-maybe-expr-wildelim: Eliminate ==? and !=? operators throughout a vl-maybe-expr-p
Vl-gateinstlist-wildelim: Eliminate ==? and !=? operators throughout a vl-gateinstlist-p.
Vl-gatedelay-wildelim: Eliminate ==? and !=? operators throughout a vl-gatedelay-p
Vl-eventcontrol-wildelim: Eliminate ==? and !=? operators throughout a vl-eventcontrol-p
Vl-enumbasetype-wildelim: Eliminate ==? and !=? operators throughout a vl-enumbasetype-p
Vl-delaycontrol-wildelim: Eliminate ==? and !=? operators throughout a vl-delaycontrol-p
Vl-arguments-wildelim: Eliminate ==? and !=? operators throughout a vl-arguments-p
Vl-vardecllist-wildelim: Eliminate ==? and !=? operators throughout a vl-vardecllist-p.
Vl-plainarg-wildelim: Eliminate ==? and !=? operators throughout a vl-plainarg-p
Vl-paramvalue-wildelim: Eliminate ==? and !=? operators throughout a vl-paramvalue-p
Vl-namedarg-wildelim: Eliminate ==? and !=? operators throughout a vl-namedarg-p
Vl-modinstlist-wildelim: Eliminate ==? and !=? operators throughout a vl-modinstlist-p.
Vl-initiallist-wildelim: Eliminate ==? and !=? operators throughout a vl-initiallist-p.
Vl-enumitem-wildelim: Eliminate ==? and !=? operators throughout a vl-enumitem-p
Vl-assignlist-wildelim: Eliminate ==? and !=? operators throughout a vl-assignlist-p.
Vl-alwayslist-wildelim: Eliminate ==? and !=? operators throughout a vl-alwayslist-p.
Vl-portlist-wildelim: Eliminate ==? and !=? operators throughout a vl-portlist-p.
Vl-exprlist-wildelim: Eliminate ==? and !=? operators throughout a vl-exprlist-p
Vl-range-wildelim: Eliminate ==? and !=? operators throughout a vl-range-p
Vl-evatom-wildelim: Eliminate ==? and !=? operators throughout a vl-evatom-p
Vl-modinst-wildelim: Eliminate ==? and !=? operators throughout a vl-modinst-p
Vl-gateinst-wildelim: Eliminate ==? and !=? operators throughout a vl-gateinst-p
Vl-vardecl-wildelim: Eliminate ==? and !=? operators throughout a vl-vardecl-p
Vl-assign-wildelim: Eliminate ==? and !=? operators throughout a vl-assign-p
Vl-portdecl-wildelim: Eliminate ==? and !=? operators throughout a vl-portdecl-p
Vl-port-wildelim: Eliminate ==? and !=? operators throughout a vl-port-p
Vl-paramdecl-wildelim: Eliminate ==? and !=? operators throughout a vl-paramdecl-p
Vl-initial-wildelim: Eliminate ==? and !=? operators throughout a vl-initial-p
Vl-always-wildelim: Eliminate ==? and !=? operators throughout a vl-always-p
Vl-module-wildelim