		Search-engine friendly clone of the ACL2 documentation.

Svex-select-part

Make-svex-select-part

Basic constructor macro for svex-select-part structures.

Syntax

(make-svex-select-part [:lsb <lsb>] 
                       [:width <width>] 
                       [:subexp <subexp>])

This is the usual way to construct svex-select-part structures. It simply conses together a structure with the specified fields.

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-svex-select-part

(defmacro make-svex-select-part (&rest args)
  (std::make-aggregate 'svex-select-part
                       args '((:lsb) (:width) (:subexp))
                       'make-svex-select-part
                       nil))

Function: svex-select-part

(defun svex-select-part (lsb width subexp)
 (declare (xargs :guard (and (svex-p lsb)
                             (natp width)
                             (svex-select-p subexp))))
 (declare (xargs :guard t))
 (let ((__function__ 'svex-select-part))
  (declare (ignorable __function__))
  (b* ((lsb (mbe :logic (svex-fix lsb) :exec lsb))
       (width (mbe :logic (nfix width) :exec width))
       (subexp (mbe :logic (svex-select-fix subexp)
                    :exec subexp)))
   (cons
        :part (std::prod-cons lsb (std::prod-cons width subexp))))))