function-symbolp

(in-package "ACL2")

(defsection std/system/function-symbolp
  :parents (std/system/event-name-queries)
  :short "Theorems about @(tsee function-symbolp)."
  (defthm function-symbolp-forward-to-symbolp
    (implies (and (function-symbolp fn wrld) (plist-worldp wrld))
      (symbolp fn))
    :rule-classes :forward-chaining))