		Search-engine friendly clone of the ACL2 documentation.

Arithmetic-operations

Op-abs

Leo absolute value operation.

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

Definitions and Theorems

Function: op-abs

(defun op-abs (arg)
  (declare (xargs :guard (valuep arg)))
  (let ((__function__ 'op-abs))
    (declare (ignorable __function__))
    (b* (((unless (member-eq (value-kind arg)
                             '(:i8 :i16 :i32 :i64 :i128)))
          (reserrf (list :op-abs (value-fix arg)))))
      (op-int-abs arg))))

Theorem: value-resultp-of-op-abs

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