		Search-engine friendly clone of the ACL2 documentation.

Vl-distitem

Make-vl-distitem

Basic constructor macro for vl-distitem structures.

Syntax

(make-vl-distitem [:left <left>] 
                  [:right <right>] 
                  [:type <type>] 
                  [:weight <weight>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-vl-distitem

(defmacro make-vl-distitem (&rest args)
  (std::make-aggregate 'vl-distitem
                       args
                       '((:left) (:right) (:type) (:weight))
                       'make-vl-distitem
                       nil))

Function: vl-distitem

(defun vl-distitem (left right type weight)
 (declare (xargs :guard (and (vl-expr-p left)
                             (vl-maybe-expr-p right)
                             (vl-distweighttype-p type)
                             (vl-expr-p weight))))
 (declare (xargs :guard t))
 (let ((__function__ 'vl-distitem))
  (declare (ignorable __function__))
  (b* ((left (mbe :logic (vl-expr-fix left)
                  :exec left))
       (right (mbe :logic (vl-maybe-expr-fix right)
                   :exec right))
       (type (mbe :logic (vl-distweighttype-fix type)
                  :exec type))
       (weight (mbe :logic (vl-expr-fix weight)
                    :exec weight)))
   (cons
      :vl-distitem (std::prod-cons (std::prod-cons left right)
                                   (std::prod-cons type weight))))))