definedp-plus

(in-package "ACL2")

(define definedp+
  ((fn symbolp) (wrld plist-worldp))
  :returns (yes/no booleanp)
  :parents (std/system/function-queries)
  :short "Enhanced variant of @(tsee definedp)."
  :long (topstring (p "This returns the same result as @(tsee definedp),
     but it causes an error if called on a symbol
     that does not name a logic-mode function.
     The reason for ensuring logic mode is that this utility
     checks whether the function has an @('unnormalized body') property,
     but the built-in program-mode functions are defined
     without having an @('unnormalized-body') property."))
  (cond ((not (function-symbolp fn wrld)) (raise "The symbol ~x0 does not name a function." fn))
    ((not (logicp fn wrld)) (raise "The function ~x0 is not in logic mode." fn))
    (t (definedp fn wrld)))
  ///
  (defthmd function-symbolp-when-definedp+
    (implies (definedp+ fn wrld) (function-symbolp fn wrld)))
  (defthmd logicp-when-definedp+
    (implies (definedp+ fn wrld) (logicp fn wrld))))