		Search-engine friendly clone of the ACL2 documentation.

Std/system/term-queries

Term-guard-obligation

Formula expressing the guard obligation of a term.

Signature
(term-guard-obligation term simplify state) → obligation
Arguments: term — Guard (pseudo-termp term).; simplify — Guard (member-eq simplify '(t :limited)).
Returns: obligation — A pseudo-termp.

The case in which term is a symbol is dealt with separately because guard-obligation interprets a symbol as a function or theorem name, not as a variable.

The simplify argument is passed to guard-obligation: see that function's documentation in this regard.

Definitions and Theorems

Function: term-guard-obligation

(defun term-guard-obligation (term simplify state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (pseudo-termp term)
                             (member-eq simplify '(t :limited)))))
 (let ((__function__ 'term-guard-obligation))
   (declare (ignorable __function__))
   (b*
    (((when (symbolp term)) *t*)
     ((mv erp val)
      (guard-obligation term
                        nil nil simplify __function__ state))
     ((when erp)
      (raise "Error ~x0 when computing the guard obligation of ~x1."
             erp term))
     (obligation-clauses (cadr val))
     (obligation-formula (termify-clause-set obligation-clauses)))
    obligation-formula)))