		Search-engine friendly clone of the ACL2 documentation.

Vttree-constraints

Make-vttree-constraints

Basic constructor macro for vttree-constraints structures.

Syntax

(make-vttree-constraints [:constraints <constraints>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-vttree-constraints

(defmacro make-vttree-constraints (&rest args)
  (std::make-aggregate 'vttree-constraints
                       args '((:constraints))
                       'make-vttree-constraints
                       nil))

Function: vttree-constraints

(defun vttree-constraints (constraints)
 (declare (xargs :guard (sv::constraintlist-p constraints)))
 (declare (xargs :guard t))
 (let ((__function__ 'vttree-constraints))
  (declare (ignorable __function__))
  (b* ((constraints (mbe :logic (sv::constraintlist-fix constraints)
                         :exec constraints)))
    (cons :constraints constraints))))