		Search-engine friendly clone of the ACL2 documentation.

Primitive

Primitive functions built into ACL2 without definitions

The ACL2 ground-zero theory includes axioms about some built-in functions that are not given explicit definitions, such as <, car, and symbolp. We sometimes call such functions primitives. The built-in constant *primitive-formals-and-guards* is an alist that associates each primitive with its list of formals and its guard; that is, each element of that alist is of the form (name formals guard). The value of this constant is displayed below.

Definition: *primitive-formals-and-guards*

(defconst *primitive-formals-and-guards*
  '((acl2-numberp (x) 't)
    (bad-atom<= (x y)
                (if (bad-atom x) (bad-atom y) 'nil))
    (binary-* (x y)
              (if (acl2-numberp x)
                  (acl2-numberp y)
                'nil))
    (binary-+ (x y)
              (if (acl2-numberp x)
                  (acl2-numberp y)
                'nil))
    (unary-- (x) (acl2-numberp x))
    (unary-/ (x)
             (if (acl2-numberp x)
                 (not (equal x '0))
               'nil))
    (< (x y)
       (if (rationalp x) (rationalp y) 'nil))
    (car (x)
         (if (consp x) 't (equal x 'nil)))
    (cdr (x)
         (if (consp x) 't (equal x 'nil)))
    (char-code (x) (characterp x))
    (characterp (x) 't)
    (code-char (x)
               (if (integerp x)
                   (if (< x '0) 'nil (< x '256))
                 'nil))
    (complex (x y)
             (if (rationalp x) (rationalp y) 'nil))
    (complex-rationalp (x) 't)
    (coerce (x y)
            (if (equal y 'list)
                (stringp x)
              (if (equal y 'string)
                  (character-listp x)
                'nil)))
    (cons (x y) 't)
    (consp (x) 't)
    (denominator (x) (rationalp x))
    (equal (x y) 't)
    (if (x y z) 't)
    (imagpart (x) (acl2-numberp x))
    (integerp (x) 't)
    (intern-in-package-of-symbol
         (str sym)
         (if (stringp str) (symbolp sym) 'nil))
    (numerator (x) (rationalp x))
    (pkg-imports (pkg) (stringp pkg))
    (pkg-witness (pkg)
                 (if (stringp pkg)
                     (not (equal pkg '""))
                   'nil))
    (rationalp (x) 't)
    (realpart (x) (acl2-numberp x))
    (stringp (x) 't)
    (symbol-name (x) (symbolp x))
    (symbol-package-name (x) (symbolp x))
    (symbolp (x) 't)))