|
|
|---|
|
|
|
|---|
Raw constructor for glmc-config-p structures.
Syntax:
(glmc-config glcp-config st-var in-vars
frame-ins rest-ins end-ins frame-in-vars
in-measure run st-hyp in-hyp bindings
bound-vars initstp nextst constr prop
st-hyp-method hints main-rewrite-rules
main-branch-merge-rules
extract-rewrite-rules
extract-branch-merge-rules)This is the lowest-level constructor for glmc-config-p structures. It simply conses together a structure with the specified fields.
Note: It's generally better to use macros like make-glmc-config or change-glmc-config instead. These macros lead to more readable and robust code, because you don't have to remember the order of the fields.
The glmc-config-p structures we create here are just constructed with ordinary cons. If you want to create honsed structures, see honsed-glmc-config instead.
This is an ordinary constructor function introduced by std::defaggregate.
Function:
(defun glmc-config (glcp-config st-var in-vars frame-ins rest-ins end-ins frame-in-vars in-measure run st-hyp in-hyp bindings bound-vars initstp nextst constr prop st-hyp-method hints main-rewrite-rules main-branch-merge-rules extract-rewrite-rules extract-branch-merge-rules) (declare (xargs :guard (and (glcp-config-p glcp-config) (variablep st-var) (variable-listp in-vars) (pseudo-term-listp frame-ins) (pseudo-term-listp rest-ins) (pseudo-termp end-ins) (variable-listp frame-in-vars) (pseudo-termp in-measure) (pseudo-termp run) (pseudo-termp st-hyp) (pseudo-termp in-hyp) (acl2::bindinglist-p bindings) (symbol-listp bound-vars) (pseudo-termp initstp) (pseudo-termp nextst) (pseudo-termp constr) (pseudo-termp prop) (st-hyp-method-p st-hyp-method)))) (cons (cons 'glcp-config glcp-config) (cons (cons 'st-var st-var) (cons (cons 'in-vars in-vars) (cons (cons 'frame-ins frame-ins) (cons (cons 'rest-ins rest-ins) (cons (cons 'end-ins end-ins) (cons (cons 'frame-in-vars frame-in-vars) (cons (cons 'in-measure in-measure) (cons (cons 'run run) (cons (cons 'st-hyp st-hyp) (cons (cons 'in-hyp in-hyp) (cons (cons 'bindings bindings) (cons (cons 'bound-vars bound-vars) (cons (cons 'initstp initstp) (cons (cons 'nextst nextst) (cons (cons 'constr constr) (cons (cons 'prop prop) (cons (cons 'st-hyp-method st-hyp-method) (cons (cons 'hints hints) (cons (cons 'main-rewrite-rules main-rewrite-rules) (cons (cons 'main-branch-merge-rules main-branch-merge-rules) (cons (cons 'extract-rewrite-rules extract-rewrite-rules) (cons (cons 'extract-branch-merge-rules extract-branch-merge-rules) nil))))))))))))))))))))))))