		Search-engine friendly clone of the ACL2 documentation.

Aij-notions

Aij-nativep

Recognize the ACL2 built-in functions natively implemented in AIJ.

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

Definitions and Theorems

Function: aij-nativep

(defun aij-nativep (fn)
  (declare (xargs :guard (symbolp fn)))
  (let ((__function__ 'aij-nativep))
    (declare (ignorable __function__))
    (and (member-eq fn *aij-natives*) t)))

Theorem: booleanp-of-aij-nativep

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