		Search-engine friendly clone of the ACL2 documentation.

Vl-inttoken-p

Vl-inttoken-constraint-p

Basic well-formedness constraint on integer tokens.

Signature
(vl-inttoken-constraint-p width value bits) → okp
Arguments: width — Guard (posp width).; value — Guard (maybe-natp value).; bits — Guard (vl-bitlist-p bits).

If the integer has a value, then it must not have bits and the value must be in bounds for its width.

If the integer has no value, then it must have exactly the right number of bits.

Definitions and Theorems

Function: vl-inttoken-constraint-p

(defun vl-inttoken-constraint-p (width value bits)
  (declare (xargs :guard (and (posp width)
                              (maybe-natp value)
                              (vl-bitlist-p bits))))
  (let ((__function__ 'vl-inttoken-constraint-p))
    (declare (ignorable __function__))
    (if value (and (not bits)
                   (< value (expt 2 width)))
      (equal (len bits) width))))