		Search-engine friendly clone of the ACL2 documentation.

Integer-operations

Minus-integer-value

Apply unary - to an integer value [C:6.5.3.3/3].

Signature
(minus-integer-value val) → resval
Arguments: val — Guard (valuep val).
Returns: resval — Type (value-resultp resval).

By the time we reach this ACL2 function, the value has been already promoted, so we put that restriction in the guard.

The type of the result is the (promoted) type of the operand [C:6.5.3.3/3], so it is the same type as the input value of this ACL2 function. We use result-integer-value to return the resulting value, or an error, as documented in that function.

Definitions and Theorems

Function: minus-integer-value

(defun minus-integer-value (val)
  (declare (xargs :guard (valuep val)))
  (declare (xargs :guard (and (value-integerp val)
                              (value-promoted-arithmeticp val))))
  (let ((__function__ 'minus-integer-value))
    (declare (ignorable __function__))
    (b* ((mathint (value-integer->get val))
         (result (- mathint))
         (resval (result-integer-value result (type-of-value val)))
         ((when (errorp resval))
          (error (list :undefined-minus (value-fix val)))))
      resval)))

Theorem: value-resultp-of-minus-integer-value

(defthm value-resultp-of-minus-integer-value
  (b* ((resval (minus-integer-value val)))
    (value-resultp resval))
  :rule-classes :rewrite)

Theorem: minus-integer-value-of-value-fix-val

(defthm minus-integer-value-of-value-fix-val
  (equal (minus-integer-value (value-fix val))
         (minus-integer-value val)))

Theorem: minus-integer-value-value-equiv-congruence-on-val

(defthm minus-integer-value-value-equiv-congruence-on-val
  (implies (value-equiv val val-equiv)
           (equal (minus-integer-value val)
                  (minus-integer-value val-equiv)))
  :rule-classes :congruence)