		Search-engine friendly clone of the ACL2 documentation.

Tree-list-tuple3

Make-tree-list-tuple3

Basic constructor macro for tree-list-tuple3 structures.

Syntax

(make-tree-list-tuple3 [:1st <1st>] 
                       [:2nd <2nd>] 
                       [:3rd <3rd>])

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

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

Definition

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

Macro: make-tree-list-tuple3

(defmacro make-tree-list-tuple3 (&rest args)
  (std::make-aggregate 'tree-list-tuple3
                       args '((:1st) (:2nd) (:3rd))
                       'make-tree-list-tuple3
                       nil))

Function: tree-list-tuple3

(defun tree-list-tuple3 (1st 2nd 3rd)
  (declare (xargs :guard (and (tree-listp 1st)
                              (tree-listp 2nd)
                              (tree-listp 3rd))))
  (declare (xargs :guard t))
  (let ((__function__ 'tree-list-tuple3))
    (declare (ignorable __function__))
    (b* ((1st (mbe :logic (tree-list-fix 1st)
                   :exec 1st))
         (2nd (mbe :logic (tree-list-fix 2nd)
                   :exec 2nd))
         (3rd (mbe :logic (tree-list-fix 3rd)
                   :exec 3rd)))
      (list (cons '1st 1st)
            (cons '2nd 2nd)
            (cons '3rd 3rd)))))