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