		Search-engine friendly clone of the ACL2 documentation.

The-number

Coerce an expected number to a number

Like fix, the-number logically returns its argument unchanged if that argument is numeric and 0 otherwise. Unlike fix, the guard for (the-number x) is (acl2-numberp x), and (the-number x) evaluates to x in raw Lisp (see guards-and-evaluation for relevant discussion).

Function: the-number

(defun the-number (x)
  (declare (xargs :guard (acl2-numberp x)))
  (mbe :logic (fix x) :exec x))