the guard proof obligation Major Section:  OTHER  See verify-
guards, and see guard for a discussion of guards. Also see
verify-guards-formula for a utility provided for viewing the
guard proof obligation, without proof. Guard-obligation is a
lower level function for use in system programs, not typically
appropriate for most ACL2 users. If you simply want to see the
guard proof obligations, see verify-guards-formula.  Example
Form: (guard-obligation 'foo nil 'top-level state) (guard-
obligation '(if (consp x) (foo (car x)) t) nil 'my-function
state)  General Forms: (guard-obligation name guard-debug ctx
state) (guard-obligation term guard-debug ctx state)  where the
first argument is either the name of a function or theorem or is
a non-variable term that may be in untranslated form; guard-
debug is typically nil but may be t (see guard-debug); ctx is a
context (typically, a symbol used in error and warning
messages); and state references the ACL2 state.  If you want to
obtain the formula but you don't care about