		Search-engine friendly clone of the ACL2 documentation.

Vl-parsed-interface-head

Make-vl-parsed-interface-head

Basic constructor macro for vl-parsed-interface-head structures.

Syntax

(make-vl-parsed-interface-head [:ifname <ifname>] 
                               [:modport <modport>])

This is the usual way to construct vl-parsed-interface-head structures. It simply conses together a structure with the specified fields.

This macro generates a new vl-parsed-interface-head structure from scratch. See also change-vl-parsed-interface-head, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-vl-parsed-interface-head

(defmacro make-vl-parsed-interface-head (&rest args)
  (std::make-aggregate 'vl-parsed-interface-head
                       args '((:ifname) (:modport))
                       'make-vl-parsed-interface-head
                       nil))

Function: vl-parsed-interface-head

(defun vl-parsed-interface-head (ifname modport)
 (declare (xargs :guard (and (stringp ifname)
                             (maybe-stringp modport))))
 (declare (xargs :guard t))
 (let ((__function__ 'vl-parsed-interface-head))
  (declare (ignorable __function__))
  (b* ((ifname (mbe :logic (str-fix ifname)
                    :exec ifname))
       (modport (mbe :logic (maybe-string-fix modport)
                     :exec modport)))
   (cons
       :vl-parsed-interface-head (std::prod-cons ifname modport)))))