		Search-engine friendly clone of the ACL2 documentation.

4vec

Make-4vec

Raw constructor for 4vecs, using cons.

(make-4vec &key upper lower) builds a 4vec with the given upper and lower.

Macro: make-4vec

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

Definitions and Theorems

Function: 4vec

(defun 4vec (upper lower)
  (declare (xargs :guard (and (integerp upper)
                              (integerp lower))))
  (b* (((the integer upper) (lifix upper))
       ((the integer lower) (lifix lower)))
    (if (eql upper lower)
        upper
      (cons upper lower))))

Theorem: 4vec-p-of-4vec

(defthm 4vec-p-of-4vec
  (equal (4vec-p (make-4vec :upper upper :lower lower))
         t))

Theorem: 4vec-of-fields

(defthm 4vec-of-fields
  (4vec-equiv (4vec (4vec->upper x) (4vec->lower x))
              x))

Theorem: 4vec-fix-is-4vec-of-fields

(defthm 4vec-fix-is-4vec-of-fields
  (equal (4vec-fix x)
         (4vec (4vec->upper x) (4vec->lower x))))

Theorem: 4vec-elim

(defthm 4vec-elim
  (implies (4vec-p x)
           (equal (4vec (4vec->upper x) (4vec->lower x))
                  x))
  :rule-classes :elim)

Theorem: 4vec-equal

(defthm 4vec-equal
  (equal (equal (4vec upper lower) x)
         (and (4vec-p x)
              (equal (4vec->upper x) (ifix upper))
              (equal (4vec->lower x) (ifix lower)))))