Basic constructor macro for deftreeops-rulename-info structures.
(make-deftreeops-rulename-info [:alt <alt>] [:nonleaf-thm <nonleaf-thm>] [:rulename-thm <rulename-thm>] [:match-thm <match-thm>] [:concs-thm <concs-thm>] [:conc-equivs-thm <conc-equivs-thm>] [:alt-kind <alt-kind>] [:check-conc-fn <check-conc-fn>] [:conc-infos <conc-infos>])
This is the usual way to construct deftreeops-rulename-info structures. It simply conses together a structure with the specified fields.
This macro generates a new deftreeops-rulename-info structure from scratch. See also change-deftreeops-rulename-info, which can "change" an existing structure, instead.
This is an ordinary
Macro:
(defmacro make-deftreeops-rulename-info (&rest args) (std::make-aggregate 'deftreeops-rulename-info args '((:alt) (:nonleaf-thm) (:rulename-thm) (:match-thm) (:concs-thm) (:conc-equivs-thm) (:alt-kind) (:check-conc-fn) (:conc-infos)) 'make-deftreeops-rulename-info nil))
Function:
(defun deftreeops-rulename-info (alt nonleaf-thm rulename-thm match-thm concs-thm conc-equivs-thm alt-kind check-conc-fn conc-infos) (declare (xargs :guard (and (alternationp alt) (common-lisp::symbolp nonleaf-thm) (common-lisp::symbolp rulename-thm) (common-lisp::symbolp match-thm) (common-lisp::symbolp concs-thm) (common-lisp::symbolp conc-equivs-thm) (natp alt-kind) (common-lisp::symbolp check-conc-fn) (deftreeops-conc-info-listp conc-infos)))) (declare (xargs :guard t)) (let ((__function__ 'deftreeops-rulename-info)) (declare (ignorable __function__)) (b* ((alt (mbe :logic (alternation-fix alt) :exec alt)) (nonleaf-thm (mbe :logic (acl2::symbol-fix nonleaf-thm) :exec nonleaf-thm)) (rulename-thm (mbe :logic (acl2::symbol-fix rulename-thm) :exec rulename-thm)) (match-thm (mbe :logic (acl2::symbol-fix match-thm) :exec match-thm)) (concs-thm (mbe :logic (acl2::symbol-fix concs-thm) :exec concs-thm)) (conc-equivs-thm (mbe :logic (acl2::symbol-fix conc-equivs-thm) :exec conc-equivs-thm)) (alt-kind (mbe :logic (nfix alt-kind) :exec alt-kind)) (check-conc-fn (mbe :logic (acl2::symbol-fix check-conc-fn) :exec check-conc-fn)) (conc-infos (mbe :logic (deftreeops-conc-info-list-fix conc-infos) :exec conc-infos))) (list (cons 'alt alt) (cons 'nonleaf-thm nonleaf-thm) (cons 'rulename-thm rulename-thm) (cons 'match-thm match-thm) (cons 'concs-thm concs-thm) (cons 'conc-equivs-thm conc-equivs-thm) (cons 'alt-kind alt-kind) (cons 'check-conc-fn check-conc-fn) (cons 'conc-infos conc-infos)))))