		Search-engine friendly clone of the ACL2 documentation.

Selfassigns

Vl-selfassign-bits

Signature
(vl-selfassign-bits name low high) → bits
Arguments: name — Guard (stringp name).; low — Guard (natp low).; high — Guard (natp high).
Returns: bits — Type (string-listp bits).

Definitions and Theorems

Function: vl-selfassign-bits

(defun vl-selfassign-bits (name low high)
  (declare (xargs :guard (and (stringp name)
                              (natp low)
                              (natp high))))
  (declare (xargs :guard (<= low high)))
  (let ((__function__ 'vl-selfassign-bits))
    (declare (ignorable __function__))
    (if (mbe :logic (zp (- (nfix high) (nfix low)))
             :exec (eql high low))
        (list (vl-selfassign-bit name low))
      (cons (vl-selfassign-bit name low)
            (vl-selfassign-bits name (+ (lnfix low) 1)
                                high)))))

Theorem: string-listp-of-vl-selfassign-bits

(defthm string-listp-of-vl-selfassign-bits
  (b* ((bits (vl-selfassign-bits name low high)))
    (string-listp bits))
  :rule-classes :rewrite)