		Search-engine friendly clone of the ACL2 documentation.

4vec

Make-honsed-4vec

Raw constructor for 4vecs, using hons.

(make-honsed-4vec &key upper lower) is identical to make-4vec except that it uses hons instead of cons. This is generally what you want when building expressions.

Macro: make-honsed-4vec

(defmacro make-honsed-4vec (&key upper lower)
  (cons 'honsed-4vec
        (cons upper (cons lower 'nil))))

Definitions and Theorems

Function: honsed-4vec

(defun honsed-4vec (upper lower)
  (declare (xargs :guard (and (integerp upper)
                              (integerp lower))))
  (mbe :logic
       (make-4vec :upper upper :lower lower)
       :exec
       (b* ((upper (lifix upper))
            (lower (lifix lower)))
         (if (eql upper lower)
             upper
           (hons upper lower)))))