		Search-engine friendly clone of the ACL2 documentation.

Deltemps

Vl-modelement-deltemps

Signature
(vl-modelement-deltemps 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-deltemps

(defun vl-modelement-deltemps (x)
  (declare (xargs :guard (vl-modelement-p x)))
  (let ((__function__ 'vl-modelement-deltemps))
    (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-deltemps x)))
           x.vl-fundecl))
        ((:vl-taskdecl)
         (b* ((x.vl-taskdecl (vl-taskdecl-deltemps x)))
           x.vl-taskdecl))
        ((:vl-modinst) (b* nil x))
        ((:vl-gateinst) (b* nil x))
        ((:vl-always)
         (b* ((x.vl-always (vl-always-deltemps x)))
           x.vl-always))
        ((:vl-initial)
         (b* ((x.vl-initial (vl-initial-deltemps x)))
           x.vl-initial))
        ((:vl-final)
         (b* ((x.vl-final (vl-final-deltemps 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* ((x.vl-assertion (vl-assertion-deltemps x)))
           x.vl-assertion))
        ((:vl-cassertion)
         (b* ((x.vl-cassertion (vl-cassertion-deltemps x)))
           x.vl-cassertion))
        ((: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-deltemps x)))
           x.vl-class))
        ((:vl-covergroup) (b* nil x))
        ((:vl-elabtask)
         (b* ((x.vl-elabtask (vl-elabtask-deltemps x)))
           x.vl-elabtask))
        (otherwise (b* nil x))))))

Theorem: vl-modelement-p-of-vl-modelement-deltemps

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

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

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

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

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