		Search-engine friendly clone of the ACL2 documentation.

Proof-obligation

Make-proof-obligation

Basic constructor macro for proof-obligation structures.

Syntax

(make-proof-obligation [:variables <variables>] 
                       [:hypotheses <hypotheses>] 
                       [:conclusion <conclusion>] 
                       [:source-expression <source-expression>])

This is the usual way to construct proof-obligation structures. It simply conses together a structure with the specified fields.

This macro generates a new proof-obligation structure from scratch. See also change-proof-obligation, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by fty::defprod.

Macro: make-proof-obligation

(defmacro make-proof-obligation (&rest args)
  (std::make-aggregate 'proof-obligation
                       args
                       '((:variables)
                         (:hypotheses)
                         (:conclusion)
                         (:source-expression))
                       'make-proof-obligation
                       nil))

Function: proof-obligation

(defun proof-obligation
       (variables hypotheses conclusion source-expression)
 (declare (xargs :guard (and (typed-variable-listp variables)
                             (obligation-hyp-listp hypotheses)
                             (expressionp conclusion)
                             (expressionp source-expression))))
 (declare (xargs :guard t))
 (let ((__function__ 'proof-obligation))
   (declare (ignorable __function__))
   (b* ((variables (mbe :logic (typed-variable-list-fix variables)
                        :exec variables))
        (hypotheses (mbe :logic (obligation-hyp-list-fix hypotheses)
                         :exec hypotheses))
        (conclusion (mbe :logic (expression-fix conclusion)
                         :exec conclusion))
        (source-expression
             (mbe :logic (expression-fix source-expression)
                  :exec source-expression)))
     (list (cons 'variables variables)
           (cons 'hypotheses hypotheses)
           (cons 'conclusion conclusion)
           (cons 'source-expression
                 source-expression)))))