Basic constructor macro for fgl-casesplit-config structures.
(make-fgl-casesplit-config [:split-params <split-params>] [:solve-params <solve-params>] [:split-concl <split-concl>] [:repeat-concl <repeat-concl>] [:allow-irrel-casesplit-vars <allow-irrel-casesplit-vars>] [:cases <cases>] [:fgl-config <fgl-config>] [:stop-on-ctrex <stop-on-ctrex>] [:stop-on-fail <stop-on-fail>])
This is the usual way to construct fgl-casesplit-config structures. It simply conses together a structure with the specified fields.
This macro generates a new fgl-casesplit-config structure from scratch. See also change-fgl-casesplit-config, which can "change" an existing structure, instead.
This is an ordinary
Macro:
(defmacro make-fgl-casesplit-config (&rest args) (std::make-aggregate 'fgl-casesplit-config args '((:split-params) (:solve-params) (:split-concl) (:repeat-concl) (:allow-irrel-casesplit-vars) (:cases) (:fgl-config) (:stop-on-ctrex) (:stop-on-fail)) 'make-fgl-casesplit-config nil))
Function:
(defun fgl-casesplit-config (split-params solve-params split-concl repeat-concl allow-irrel-casesplit-vars cases fgl-config stop-on-ctrex stop-on-fail) (declare (xargs :guard (and (casesplit-alist-p cases) (fgl-config-p fgl-config)))) (declare (xargs :guard t)) (let ((__function__ 'fgl-casesplit-config)) (declare (ignorable __function__)) (b* ((cases (mbe :logic (casesplit-alist-fix cases) :exec cases)) (fgl-config (mbe :logic (fgl-config-fix fgl-config) :exec fgl-config))) (list (cons 'split-params split-params) (cons 'solve-params solve-params) (cons 'split-concl split-concl) (cons 'repeat-concl repeat-concl) (cons 'allow-irrel-casesplit-vars allow-irrel-casesplit-vars) (cons 'cases cases) (cons 'fgl-config fgl-config) (cons 'stop-on-ctrex stop-on-ctrex) (cons 'stop-on-fail stop-on-fail)))))