Basic constructor macro for proof-tree-equal structures.
(make-proof-tree-equal [:asg <asg>] [:left <left>] [:right <right>])
This is the usual way to construct proof-tree-equal structures. It simply conses together a structure with the specified fields.
This macro generates a new proof-tree-equal structure from scratch. See also change-proof-tree-equal, which can "change" an existing structure, instead.
This is an ordinary
Macro:
(defmacro make-proof-tree-equal (&rest args) (std::make-aggregate 'proof-tree-equal args '((:asg) (:left) (:right)) 'make-proof-tree-equal nil))
Function:
(defun proof-tree-equal (asg left right) (declare (xargs :guard (and (assignmentp asg) (expressionp left) (expressionp right)))) (declare (xargs :guard t)) (let ((__function__ 'proof-tree-equal)) (declare (ignorable __function__)) (b* ((asg (mbe :logic (assignment-fix asg) :exec asg)) (left (mbe :logic (expression-fix left) :exec left)) (right (mbe :logic (expression-fix right) :exec right))) (cons :equal (list asg left right)))))