		Search-engine friendly clone of the ACL2 documentation.

Integer-operations

Plus-integer-value

Apply unary + to an integer value [C:6.5.3.3/2].

Signature
(plus-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.

Since the value is already promoted, this function returns the value unchanged. We introduce this function mainly for uniformity with other operations, despite it being trivial in a way.

Definitions and Theorems

Function: plus-integer-value

(defun plus-integer-value (val)
  (declare (xargs :guard (valuep val)))
  (declare (xargs :guard (and (value-integerp val)
                              (value-promoted-arithmeticp val))))
  (let ((__function__ 'plus-integer-value))
    (declare (ignorable __function__))
    (value-fix val)))

Theorem: value-resultp-of-plus-integer-value

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

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

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

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

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