		Search-engine friendly clone of the ACL2 documentation.

Vl-udpline

Make-vl-udpline

Basic constructor macro for vl-udpline structures.

Syntax

(make-vl-udpline [:inputs <inputs>] 
                 [:output <output>] 
                 [:current <current>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-vl-udpline

(defmacro make-vl-udpline (&rest args)
  (std::make-aggregate 'vl-udpline
                       args '((:inputs) (:output) (:current))
                       'make-vl-udpline
                       nil))

Function: vl-udpline

(defun vl-udpline (inputs output current)
 (declare (xargs :guard (and (vl-udpentrylist-p inputs)
                             (vl-udpsymbol-p output)
                             (vl-maybe-udpsymbol-p-p current))))
 (declare (xargs :guard t))
 (let ((__function__ 'vl-udpline))
  (declare (ignorable __function__))
  (b* ((inputs (mbe :logic (vl-udpentrylist-fix inputs)
                    :exec inputs))
       (output (mbe :logic (vl-udpsymbol-fix output)
                    :exec output))
       (current (mbe :logic (vl-maybe-udpsymbol-p-fix current)
                     :exec current)))
   (cons
    :vl-udpline (std::prod-cons inputs
                                (std::prod-cons output current))))))