		Search-engine friendly clone of the ACL2 documentation.

Proof-obligation

Change-proof-obligation

Modifying constructor for proof-obligation structures.

Syntax

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

This is an often useful alternative to make-proof-obligation.

We construct a new proof-obligation structure that is a copy of x, except that you can explicitly change some particular fields. Any fields you don't mention just keep their values from x.

Definition

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

Macro: change-proof-obligation

(defmacro change-proof-obligation (x &rest args)
  (std::change-aggregate
       'proof-obligation
       x args
       '((:variables . proof-obligation->variables)
         (:hypotheses . proof-obligation->hypotheses)
         (:conclusion . proof-obligation->conclusion)
         (:source-expression . proof-obligation->source-expression))
       'change-proof-obligation
       'nil))