		Search-engine friendly clone of the ACL2 documentation.

Std/system/function-queries

Primitivep+

Enhanced variant of primitivep.

Signature
(primitivep+ fn wrld) → yes/no
Arguments: fn — Guard (symbolp fn).; wrld — Guard (plist-worldp wrld).
Returns: yes/no — Type (booleanp yes/no).

This returns the same result as primitivep, but it causes an error if called on a symbol that does not name a function. This check requires an extra world argument (compared to primitivep), which is usually available when doing system programming.

Definitions and Theorems

Function: primitivep+

(defun primitivep+ (fn wrld)
  (declare (xargs :guard (and (symbolp fn) (plist-worldp wrld))))
  (let ((__function__ 'primitivep+))
    (declare (ignorable __function__))
    (if (not (function-symbolp fn wrld))
        (raise "The symbol ~x0 does not name a function."
               fn)
      (primitivep fn))))

Theorem: booleanp-of-primitivep+

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