|
|
|---|
|
|
|
|---|
Constructor macro for glmc-config-p structures.
Syntax:
(make-glmc-config [:glcp-config <glcp-config>]
[:st-var <st-var>]
[:in-vars <in-vars>]
[:frame-ins <frame-ins>]
[:rest-ins <rest-ins>]
[:end-ins <end-ins>]
[:frame-in-vars <frame-in-vars>]
[:in-measure <in-measure>]
[:run <run>]
[:st-hyp <st-hyp>]
[:in-hyp <in-hyp>]
[:bindings <bindings>]
[:bound-vars <bound-vars>]
[:initstp <initstp>]
[:nextst <nextst>]
[:constr <constr>]
[:prop <prop>]
[:st-hyp-method <st-hyp-method>]
[:hints <hints>]
[:main-rewrite-rules <main-rewrite-rules>]
[:main-branch-merge-rules <main-branch-merge-rules>]
[:extract-rewrite-rules <extract-rewrite-rules>]
[:extract-branch-merge-rules <extract-branch-merge-rules>])
This is our preferred way to construct glmc-config-p structures. It simply conses together a structure with the specified fields.
This macro generates a new glmc-config-p structure from scratch. See also change-glmc-config, which can "change" an existing structure, instead.
The glmc-config-p structures we create here are just constructed with ordinary cons. If you want to create honsed structures, see make-honsed-glmc-config instead.
This is an ordinary
Macro:
(defmacro make-glmc-config (&rest args) (std::make-aggregate 'glmc-config args '((:glcp-config make-glcp-config) (:st-var quote acl2::st) (:in-vars quote (acl2::ins)) (:frame-ins quote ((car acl2::ins))) (:rest-ins quote ((cdr acl2::ins))) (:end-ins quote (not (consp acl2::ins))) (:frame-in-vars quote (acl2::in)) (:in-measure quote (len acl2::ins)) (:run) (:st-hyp) (:in-hyp) (:bindings) (:bound-vars) (:initstp) (:nextst) (:constr) (:prop) (:st-hyp-method quote nil) (:hints) (:main-rewrite-rules quote :default) (:main-branch-merge-rules quote :default) (:extract-rewrite-rules quote :default) (:extract-branch-merge-rules quote :default)) 'make-glmc-config nil))