|
|
|---|
|
|
|
|---|
Constructor macro for honsed eqbylbp-config-p structures.
Syntax:
(make-honsed-eqbylbp-config [:restriction <restriction>]
[:witness-rule <witness-rule>]
[:instance-rule <instance-rule>]
[:prune-examples <prune-examples>]
[:passes <passes>]
[:simp-hint <simp-hint>]
[:add-hints <add-hints>]
[:verbosep <verbosep>])
This is identical to make-eqbylbp-config, except that we hons the structure we are creating.
This is an ordinary honsing
Macro:
(defmacro make-honsed-eqbylbp-config (&rest args) (std::make-aggregate 'eqbylbp-config args '((:restriction) (:witness-rule) (:instance-rule) (:prune-examples) (:passes) (:simp-hint) (:add-hints) (:verbosep)) 'make-honsed-eqbylbp-config t))