		Search-engine friendly clone of the ACL2 documentation.

Vl-range

Make-vl-range

Basic constructor macro for vl-range structures.

Syntax

(make-vl-range [:msb <msb>] 
               [:lsb <lsb>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-vl-range

(defmacro make-vl-range (&rest args)
  (std::make-aggregate 'vl-range
                       args '((:msb) (:lsb))
                       'make-vl-range
                       nil))

Function: vl-range

(defun vl-range (msb lsb)
  (declare (xargs :guard (and (vl-expr-p msb) (vl-expr-p lsb))))
  (declare (xargs :guard t))
  (let ((__function__ 'vl-range))
    (declare (ignorable __function__))
    (b* ((msb (mbe :logic (vl-expr-fix msb)
                   :exec msb))
         (lsb (mbe :logic (vl-expr-fix lsb)
                   :exec lsb)))
      (cons :vl-range (std::prod-cons msb lsb)))))