		Search-engine friendly clone of the ACL2 documentation.

Proof-tree-relation

Make-proof-tree-relation

Basic constructor macro for proof-tree-relation structures.

Syntax

(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.

Definition

This is an ordinary make- macro introduced by fty::defprod.

Macro: make-proof-tree-relation

(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: proof-tree-relation

(defun proof-tree-relation (asg name args sub asgfree)
  (declare (xargs :guard (and (assignmentp asg)
                              (namep 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 (name-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)))))