		Search-engine friendly clone of the ACL2 documentation.

Integer-operations

Plus-integer-value

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

Signature
(plus-integer-value val) → resval
Arguments: val — Guard (valuep val).
Returns: resval — Type (valuep 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: valuep-of-plus-integer-value

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

Theorem: type-of-value-of-plus-integer-value

(defthm type-of-value-of-plus-integer-value
  (b* ((?resval (plus-integer-value val)))
    (equal (type-of-value resval)
           (type-of-value val))))

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)