		Search-engine friendly clone of the ACL2 documentation.

Increment-elim

Vl-modelement-increwrite

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

Definitions and Theorems

Function: vl-modelement-increwrite

(defun vl-modelement-increwrite (x)
  (declare (xargs :guard (vl-modelement-p x)))
  (let ((__function__ 'vl-modelement-increwrite))
    (declare (ignorable __function__))
    (let ((x (vl-modelement-fix x)))
      (common-lisp::case (tag x)
        ((:vl-portdecl) (b* nil x))
        ((:vl-assign) (b* nil x))
        ((:vl-alias) (b* nil x))
        ((:vl-vardecl) (b* nil x))
        ((:vl-paramdecl) (b* nil x))
        ((:vl-fundecl)
         (b* ((x.vl-fundecl (vl-fundecl-increwrite x)))
           x.vl-fundecl))
        ((:vl-taskdecl)
         (b* ((x.vl-taskdecl (vl-taskdecl-increwrite x)))
           x.vl-taskdecl))
        ((:vl-modinst) (b* nil x))
        ((:vl-gateinst) (b* nil x))
        ((:vl-always)
         (b* ((x.vl-always (vl-always-increwrite x)))
           x.vl-always))
        ((:vl-initial)
         (b* ((x.vl-initial (vl-initial-increwrite x)))
           x.vl-initial))
        ((:vl-final)
         (b* ((x.vl-final (vl-final-increwrite x)))
           x.vl-final))
        ((:vl-typedef) (b* nil x))
        ((:vl-import) (b* nil x))
        ((:vl-fwdtypedef) (b* nil x))
        ((:vl-modport) (b* nil x))
        ((:vl-genvar) (b* nil x))
        ((:vl-assertion) (b* nil x))
        ((:vl-cassertion) (b* nil x))
        ((:vl-property) (b* nil x))
        ((:vl-sequence) (b* nil x))
        ((:vl-clkdecl) (b* nil x))
        ((:vl-gclkdecl) (b* nil x))
        ((:vl-defaultdisable) (b* nil x))
        ((:vl-dpiimport) (b* nil x))
        ((:vl-dpiexport) (b* nil x))
        ((:vl-bind) (b* nil x))
        ((:vl-class)
         (b* ((x.vl-class (vl-class-increwrite x)))
           x.vl-class))
        ((:vl-covergroup) (b* nil x))
        ((:vl-elabtask)
         (b* ((x.vl-elabtask (vl-elabtask-increwrite x)))
           x.vl-elabtask))
        (otherwise (b* nil x))))))

Theorem: vl-modelement-p-of-vl-modelement-increwrite

(defthm vl-modelement-p-of-vl-modelement-increwrite
  (b* ((new-x (vl-modelement-increwrite x)))
    (vl-modelement-p new-x))
  :rule-classes :rewrite)

Theorem: vl-modelement-increwrite-of-vl-modelement-fix-x

(defthm vl-modelement-increwrite-of-vl-modelement-fix-x
  (equal (vl-modelement-increwrite (vl-modelement-fix x))
         (vl-modelement-increwrite x)))

Theorem: vl-modelement-increwrite-vl-modelement-equiv-congruence-on-x

(defthm vl-modelement-increwrite-vl-modelement-equiv-congruence-on-x
  (implies (vl-modelement-equiv x x-equiv)
           (equal (vl-modelement-increwrite x)
                  (vl-modelement-increwrite x-equiv)))
  :rule-classes :congruence)