|
|
|---|
|
|
|
|---|
Modifying constructor for outcome-proof-obligation-failure structures.
(change-outcome-proof-obligation-failure x
[:message <message>]
[:obligation-expr <obligation-expr>])
This is an often useful alternative to make-outcome-proof-obligation-failure.
We construct a new outcome-proof-obligation-failure structure that is a copy of
This is an ordinary
Macro:
(defmacro change-outcome-proof-obligation-failure (x &rest args) (std::change-aggregate 'outcome-proof-obligation-failure x args '((:message . outcome-proof-obligation-failure->message) (:obligation-expr . outcome-proof-obligation-failure->obligation-expr)) 'change-outcome-proof-obligation-failure 'nil))