no-stobjs-p

(in-package "ACL2")

(define no-stobjs-p
  ((fn symbolp) (wrld plist-worldp))
  :guard (not (member-eq fn *stobjs-out-invalid*))
  :returns (yes/no booleanp)
  :verify-guards nil
  :parents (std/system/function-queries)
  :short "Check if a named function has no input or output @(see stobj)s."
  :long (topstring (p "The function must not be in @('*stobjs-out-invalid*'),
     because in that case its (output) stobjs depend on how it is called.")
    (p "See @(tsee no-stobjs-p+) for an enhanced variant of this utility."))
  (and (all-nils (stobjs-in fn wrld))
    (all-nils (stobjs-out fn wrld))))