A copying macro that lets you create new wcp-witness-rule-p structures, based on existing structures.
Syntax:
(change-wcp-witness-rule x [:name <name>] [:enabledp <enabledp>] [:term <term>] [:expr <expr>] [:restriction <restriction>] [:theorem <theorem>] [:generalize <generalize>])
This is a sometimes useful alternative to make-wcp-witness-rule.
It constructs a new wcp-witness-rule-p structure that is a copy of
This is an ordinary
Macro:
(defmacro change-wcp-witness-rule (x &rest args) (std::change-aggregate 'wcp-witness-rule x args '((:name . wcp-witness-rule->name) (:enabledp . wcp-witness-rule->enabledp) (:term . wcp-witness-rule->term) (:expr . wcp-witness-rule->expr) (:restriction . wcp-witness-rule->restriction) (:theorem . wcp-witness-rule->theorem) (:generalize . wcp-witness-rule->generalize)) 'change-wcp-witness-rule 'nil))