Modifying constructor for maybe-proof-obligation-none structures.
(change-maybe-proof-obligation-none x )
This is an often useful alternative to make-maybe-proof-obligation-none.
We construct a new maybe-proof-obligation-none structure that is a copy of
This is an ordinary
Macro:
(defmacro change-maybe-proof-obligation-none (x &rest args) (std::change-aggregate 'maybe-proof-obligation-none x args 'nil 'change-maybe-proof-obligation-none 'nil))