rawp

(in-package "ACL2")

(define rawp
  ((fn symbolp) state)
  :returns (yes/no booleanp)
  :verify-guards nil
  :parents (std/system/function-queries)
  :short "Check if a named function has raw Lisp code."
  :long (topstring (p "The global variables
     @('logic-fns-with-raw-code') and @('program-fns-with-raw-code')
     list the logic-mode and program-mode functions with raw Lisp code.
     Their initial values are
     @('*initial-logic-fns-with-raw-code*') and
     @('*initial-program-fns-with-raw-code*'),
     but they may change if functions with raw Lisp code are introduced.")
    (p "This function checks whether a function has raw Lisp code
     by checking whether it is listed in one of those global variables."))
  (and (or (member-eq fn (@ logic-fns-with-raw-code))
      (member-eq fn (@ program-fns-with-raw-code)))
    t))