		Search-engine friendly clone of the ACL2 documentation.

Integer-arithmetic-operations

Op-int-neg

Leo integer negation operation.

Signature
(op-int-neg arg) → result
Arguments: arg — Guard (int-valuep arg).
Returns: result — Type (value-resultp result).

Definitions and Theorems

Function: op-int-neg

(defun op-int-neg (arg)
  (declare (xargs :guard (int-valuep arg)))
  (let ((__function__ 'op-int-neg))
    (declare (ignorable __function__))
    (b* ((err (reserrf (list :op-int-neg (value-fix arg)))))
      (case (value-kind arg)
        (:i8 (b* ((res (- (value-i8->get arg))))
               (if (sbyte8p res) (value-i8 res) err)))
        (:i16 (b* ((res (- (value-i16->get arg))))
                (if (sbyte16p res)
                    (value-i16 res)
                  err)))
        (:i32 (b* ((res (- (value-i32->get arg))))
                (if (sbyte32p res)
                    (value-i32 res)
                  err)))
        (:i64 (b* ((res (- (value-i64->get arg))))
                (if (sbyte64p res)
                    (value-i64 res)
                  err)))
        (:i128 (b* ((res (- (value-i128->get arg))))
                 (if (sbyte128p res)
                     (value-i128 res)
                   err)))
        (t err)))))

Theorem: value-resultp-of-op-int-neg

(defthm value-resultp-of-op-int-neg
  (b* ((result (op-int-neg arg)))
    (value-resultp result))
  :rule-classes :rewrite)

Theorem: op-int-neg-of-value-fix-arg

(defthm op-int-neg-of-value-fix-arg
  (equal (op-int-neg (value-fix arg))
         (op-int-neg arg)))

Theorem: op-int-neg-value-equiv-congruence-on-arg

(defthm op-int-neg-value-equiv-congruence-on-arg
  (implies (value-equiv arg arg-equiv)
           (equal (op-int-neg arg)
                  (op-int-neg arg-equiv)))
  :rule-classes :congruence)