primitivep

(in-package "ACL2")

(define primitivep
  ((fn symbolp))
  :returns (yes/no booleanp)
  :parents (std/system/function-queries)
  :short "Check if a named function is @(see primitive)."
  :long (topstring-p "See @(tsee primitivep+) for an enhanced variant of this utility.")
  (and (member-eq fn (strip-cars *primitive-formals-and-guards*))
    t)
  ///
  (defthm primitivep-forward-to-symbolp
    (implies (primitivep fn) (symbolp fn))
    :rule-classes :forward-chaining))