lambda-guard-verified-fnsp

(in-package "ACL2")

(define lambda-guard-verified-fnsp
  ((lambd pseudo-lambdap) (wrld plist-worldp))
  :returns (yes/no booleanp)
  :parents (std/system/term-queries)
  :short "Check if all the functions in a lambda expression
          are guard-verified."
  :long (topstring (p "The name of this function is consistent with
     the name of @(tsee guard-verified-fnsp).")
    (p "Note that if any function
     inside the @(':logic') component of an @(tsee mbe)
     or called via @(tsee ec-call)
     is not guard-verified,
     we return @('nil'),
     even when @('lambd') could otherwise be fully guard-verified.
     See @(tsee lambda-guard-verified-exec-fnsp) for a similar utility
     that ignores the guard verification status of functions
     in the @(':logic') components of @(tsee mbe)s
     or called via @(tsee ec-call)."))
  (guard-verified-fnsp (lambda-body lambd) wrld)
  :guard-hints (("Goal" :in-theory (enable pseudo-lambdap))))