• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Hons-and-memoization
    • Events
    • History
    • Parallelism
    • Programming
      • Defun
      • Declare
      • System-utilities
      • Stobj
      • State
      • Memoize
      • Mbe
      • Io
      • Apply$
      • Defpkg
      • Mutual-recursion
      • Loop$
      • Programming-with-state
      • Arrays
      • Characters
      • Time$
      • Loop$-primer
      • Fast-alists
      • Defmacro
      • Defconst
      • Evaluation
      • Guard
      • Equality-variants
      • Compilation
      • Hons
      • ACL2-built-ins
      • Developers-guide
      • System-attachments
      • Advanced-features
      • Set-check-invariant-risk
      • Numbers
      • Irrelevant-formals
      • Efficiency
      • Introduction-to-programming-in-ACL2-for-those-who-know-lisp
      • Redefining-programs
      • Lists
      • Invariant-risk
      • Errors
      • Defabbrev
      • Conses
      • Alists
      • Set-register-invariant-risk
      • Strings
      • Program-wrapper
      • Get-internal-time
      • Basics
      • Packages
      • Defmacro-untouchable
      • Primitive
      • <<
      • Revert-world
      • Set-duplicate-keys-action
      • Unmemoize
      • Symbols
      • Def-list-constructor
      • Easy-simplify-term
      • Defiteration
      • Defopen
      • Sleep
    • Start-here
    • Real
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Programming
• ACL2-built-ins

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)))