		Search-engine friendly clone of the ACL2 documentation.

Std/system/function-queries

Primitivep

Check if a named function is primitive.

Signature
(primitivep fn) → yes/no
Arguments: fn — Guard (symbolp fn).
Returns: yes/no — Type (booleanp yes/no).

See primitivep+ for an enhanced variant of this utility.

Definitions and Theorems

Function: primitivep

(defun primitivep (fn)
  (declare (xargs :guard (symbolp fn)))
  (let ((__function__ 'primitivep))
    (declare (ignorable __function__))
    (and (member-eq fn
                    (strip-cars *primitive-formals-and-guards*))
         t)))

Theorem: booleanp-of-primitivep

(defthm booleanp-of-primitivep
  (b* ((yes/no (primitivep fn)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: primitivep-forward-to-symbolp

(defthm primitivep-forward-to-symbolp
  (implies (primitivep fn) (symbolp fn))
  :rule-classes :forward-chaining)