		Search-engine friendly clone of the ACL2 documentation.

Operations

Shr-values

Apply >> to values [C17:6.5.7/2] [C17:6.5.7/3] [C17:6.5.7/5].

Signature
(shr-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: shr-values

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

Theorem: value-resultp-of-shr-values

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

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

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

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

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

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

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

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

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