guard-verified-p

(in-package "ACL2")

(define guard-verified-p
  ((fn/thm symbolp) (wrld plist-worldp))
  :returns (yes/no booleanp)
  :parents (std/system/function-queries std/system/theorem-queries)
  :short "Check if a named function or theorem is @(tsee guard)-verified."
  :long (topstring-p "See @(tsee guard-verified-p+) for
    an enhanced variant of this utility.")
  (eq (symbol-class fn/thm wrld) :common-lisp-compliant))