uguard

(in-package "ACL2")

(define uguard
  ((fn pseudo-termfnp) (wrld plist-worldp))
  :returns (guard "A @(tsee pseudo-termp).")
  :parents (std/system/function-queries)
  :short "Unoptimized guard of a named function or of a lambda expression."
  :long (topstring (p "This is a specialization of "
      (seetopic "system-utilities" "@('guard')")
      " with @('nil') as the second argument.
     Since @(tsee guard) is in program mode only because of
     the code that handles the case in which
     the second argument is non-@('nil'),
     we avoid calling @(tsee guard) and instead replicate
     the code that handles the case in which the second argument is @('nil');
     thus, this utility is in logic mode and guard-verified.")
    (p "See @(tsee uguard+) for an enhanced variant of this utility."))
  (cond ((symbolp fn) (getpropc fn 'guard *t* wrld)) (t *t*)))