		Search-engine friendly clone of the ACL2 documentation.

Vl-inttoken-p

Honsed-vl-inttoken

Raw constructor for honsed vl-inttoken-p structures.

Syntax:

(honsed-vl-inttoken etext width 
                    signedp value bits wasunsized breakp)

This is identical to vl-inttoken, except that we hons the structure we are creating.

Definition

This is an ordinary honsing constructor introduced by defaggregate.

Function: honsed-vl-inttoken

(defun honsed-vl-inttoken
       (etext width
              signedp value bits wasunsized breakp)
 (declare
   (xargs :guard (and (and (vl-echarlist-p etext)
                           (consp etext))
                      (posp width)
                      (booleanp signedp)
                      (maybe-natp value)
                      (vl-bitlist-p bits)
                      (booleanp wasunsized)
                      (booleanp breakp)
                      (vl-inttoken-constraint-p width value bits))))
 (mbe
  :logic (vl-inttoken etext width
                      signedp value bits wasunsized breakp)
  :exec
  (hons :vl-inttoken
        (std::prod-hons
             (std::prod-hons etext (std::prod-hons width signedp))
             (std::prod-hons (std::prod-hons value bits)
                             (std::prod-hons wasunsized breakp))))))