logic-function-namep

(in-package "ACL2")

(define logic-function-namep
  (x (wrld plist-worldp))
  :returns (yes/no booleanp)
  :parents (std/system/event-name-queries)
  :short "Recognize symbols that name logic-mode functions."
  :long (topstring-p "This function is enabled because it is meant as an abbreviation.
    Theorems triggered by this function should be generally avoided.")
  (and (function-namep x wrld) (logicp x wrld))
  :enabled t)