		Search-engine friendly clone of the ACL2 documentation.

Operations

Shl-values

Apply << to values [C17:6.5.7/2] [C17:6.5.7/3] [C17:6.5.7/4].

Signature
(shl-values val1 val2) → resval
Arguments: val1 — Guard (valuep val1).; val2 — Guard (valuep val2).
Returns: resval — Type (value-resultp resval).

It is an error if the values are not integers. If they are integers, we promote them and then we call the operation on integer values.

Definitions and Theorems

Function: shl-values

(defun shl-values (val1 val2)
  (declare (xargs :guard (and (valuep val1) (valuep val2))))
  (let ((__function__ 'shl-values))
    (declare (ignorable __function__))
    (if (and (value-integerp val1)
             (value-integerp val2))
        (shl-integer-values (promote-value val1)
                            (promote-value val2))
      (error (list :shl-mistype :required :integer
                   :integer :supplied (value-fix val1)
                   (value-fix val2))))))

Theorem: value-resultp-of-shl-values

(defthm value-resultp-of-shl-values
  (b* ((resval (shl-values val1 val2)))
    (value-resultp resval))
  :rule-classes :rewrite)

Theorem: shl-values-of-value-fix-val1

(defthm shl-values-of-value-fix-val1
  (equal (shl-values (value-fix val1) val2)
         (shl-values val1 val2)))

Theorem: shl-values-value-equiv-congruence-on-val1

(defthm shl-values-value-equiv-congruence-on-val1
  (implies (value-equiv val1 val1-equiv)
           (equal (shl-values val1 val2)
                  (shl-values val1-equiv val2)))
  :rule-classes :congruence)

Theorem: shl-values-of-value-fix-val2

(defthm shl-values-of-value-fix-val2
  (equal (shl-values val1 (value-fix val2))
         (shl-values val1 val2)))

Theorem: shl-values-value-equiv-congruence-on-val2

(defthm shl-values-value-equiv-congruence-on-val2
  (implies (value-equiv val2 val2-equiv)
           (equal (shl-values val1 val2)
                  (shl-values val1 val2-equiv)))
  :rule-classes :congruence)