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