Modifying constructor for atj-test-value-ACL2 structures.
(change-atj-test-value-ACL2 x [:get <get>])
This is an often useful alternative to make-atj-test-value-ACL2.
We construct a new atj-test-value-ACL2 structure that is a copy of
This is an ordinary
Macro:
(defmacro change-atj-test-value-acl2 (x &rest args) (std::change-aggregate 'atj-test-value-acl2 x args '((:get . atj-test-value-acl2->get)) 'change-atj-test-value-acl2 'nil))