		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)