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