		Search-engine friendly clone of the ACL2 documentation.

Tree-nonleaf

Make-tree-nonleaf

Basic constructor macro for tree-nonleaf structures.

Syntax

(make-tree-nonleaf [:rulename? <rulename?>] 
                   [:branches <branches>])

This is the usual way to construct tree-nonleaf structures. It simply conses together a structure with the specified fields.

This macro generates a new tree-nonleaf structure from scratch. See also change-tree-nonleaf, which can "change" an existing structure, instead.

Definition

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

Macro: make-tree-nonleaf

(defmacro make-tree-nonleaf (&rest args)
  (std::make-aggregate 'tree-nonleaf
                       args '((:rulename?) (:branches))
                       'make-tree-nonleaf
                       nil))

Function: tree-nonleaf

(defun tree-nonleaf (rulename? branches)
  (declare (xargs :guard (and (rulename-optionp rulename?)
                              (tree-list-listp branches))))
  (declare (xargs :guard t))
  (let ((__function__ 'tree-nonleaf))
    (declare (ignorable __function__))
    (b* ((rulename? (mbe :logic (rulename-option-fix rulename?)
                         :exec rulename?))
         (branches (mbe :logic (tree-list-list-fix branches)
                        :exec branches)))
      (cons :nonleaf (list rulename? branches)))))