		Search-engine friendly clone of the ACL2 documentation.

Udp-elim

Vl-udp-vardecl-from-portdecl

Signature
(vl-udp-vardecl-from-portdecl x) → vardecl
Arguments: x — Guard (vl-portdecl-p x).
Returns: vardecl — Type (vl-vardecl-p vardecl).

Definitions and Theorems

Function: vl-udp-vardecl-from-portdecl

(defun
 vl-udp-vardecl-from-portdecl (x)
 (declare (xargs :guard (vl-portdecl-p x)))
 (let ((__function__ 'vl-udp-vardecl-from-portdecl))
      (declare (ignorable __function__))
      (b* (((vl-portdecl x)))
          (make-vl-vardecl :name x.name
                           :type x.type
                           :nettype :vl-wire
                           :atts (cons (cons "VL_PORT_IMPLICIT" nil)
                                       x.atts)
                           :loc x.loc))))

Theorem: vl-vardecl-p-of-vl-udp-vardecl-from-portdecl

(defthm vl-vardecl-p-of-vl-udp-vardecl-from-portdecl
        (b* ((vardecl (vl-udp-vardecl-from-portdecl x)))
            (vl-vardecl-p vardecl))
        :rule-classes :rewrite)