Abs
The absolute value of a real number
(Abs x) is -x if x is negative and is x
otherwise.
The guard for abs requires its argument to be a rational (real, in ACL2(r)) number.
Abs is a Common Lisp function. See any Common Lisp documentation for
more information.
From ``Common Lisp the Language'' page 205, we must not allow complex
x as an argument to abs in ACL2, because if we did we would have to
return a number that might be a floating point number and hence not an ACL2
object.
Function: abs
(defun abs (x)
(declare (xargs :guard (real/rationalp x)))
(if (minusp x) (- x) x))
