definedp

(in-package "ACL2")

(define definedp
  ((fn symbolp) (wrld plist-worldp))
  :returns (yes/no booleanp)
  :parents (std/system/function-queries)
  :short "Check if a named logic-mode function is defined."
  :long (topstring (p "We check if the function symbol has an @('unnormalized-body') property.")
    (p "The built-in program-mode functions are defined
     but do not have an @('unnormalized-body') property.
     This is why this utility should only be used on logic-mode functions.")
    (p "See @(tsee definedp+) for an enhanced variant of this utility."))
  (if (getpropc fn 'unnormalized-body nil wrld)
    t
    nil))