constant-symbolp

(in-package "ACL2")

(define constant-symbolp
  ((sym symbolp) (wrld plist-worldp))
  :returns (yes/no booleanp)
  :parents (std/system/event-name-queries)
  :short "Check if a symbol names a constant,
          i.e. it has a @('const') property."
  :long (topstring-p "This function is named in analogy to
    the @(tsee function-symbolp) built-in system utility.")
  (not (eq (getpropc sym 'const t wrld) t))
  ///
  (defthm constant-symbolp-forward-to-symbolp
    (implies (and (constant-symbolp fn wrld) (plist-worldp wrld))
      (symbolp fn))
    :rule-classes :forward-chaining))