		Search-engine friendly clone of the ACL2 documentation.

Vttree-branch

Change-vttree-branch

Modifying constructor for vttree-branch structures.

Syntax

(change-vttree-branch x 
                      [:left <left>] 
                      [:right <right>])

This is an often useful alternative to make-vttree-branch.

We construct a new vttree-branch structure that is a copy of x, except that you can explicitly change some particular fields. Any fields you don't mention just keep their values from x.

Definition

This is an ordinary change- macro introduced by defprod.

Macro: change-vttree-branch

(defmacro change-vttree-branch (x &rest args)
  (std::change-aggregate 'vttree-branch
                         x args
                         '((:left . vttree-branch->left)
                           (:right . vttree-branch->right))
                         'change-vttree-branch
                         'nil))