		Search-engine friendly clone of the ACL2 documentation.

Tree-list-tuple9

Make-tree-list-tuple9

Basic constructor macro for tree-list-tuple9 structures.

Syntax

(make-tree-list-tuple9 [:1st <1st>] 
                       [:2nd <2nd>] 
                       [:3rd <3rd>] 
                       [:4th <4th>] 
                       [:5th <5th>] 
                       [:6th <6th>] 
                       [:7th <7th>] 
                       [:8th <8th>] 
                       [:9th <9th>])

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

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

Definition

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

Macro: make-tree-list-tuple9

(defmacro make-tree-list-tuple9 (&rest args)
  (std::make-aggregate 'tree-list-tuple9
                       args
                       '((:1st)
                         (:2nd)
                         (:3rd)
                         (:4th)
                         (:5th)
                         (:6th)
                         (:7th)
                         (:8th)
                         (:9th))
                       'make-tree-list-tuple9
                       nil))

Function: tree-list-tuple9

(defun tree-list-tuple9 (1st 2nd 3rd 4th 5th 6th 7th 8th 9th)
  (declare (xargs :guard (and (tree-listp 1st)
                              (tree-listp 2nd)
                              (tree-listp 3rd)
                              (tree-listp 4th)
                              (tree-listp 5th)
                              (tree-listp 6th)
                              (tree-listp 7th)
                              (tree-listp 8th)
                              (tree-listp 9th))))
  (declare (xargs :guard t))
  (let ((__function__ 'tree-list-tuple9))
    (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))
         (4th (mbe :logic (tree-list-fix 4th)
                   :exec 4th))
         (5th (mbe :logic (tree-list-fix 5th)
                   :exec 5th))
         (6th (mbe :logic (tree-list-fix 6th)
                   :exec 6th))
         (7th (mbe :logic (tree-list-fix 7th)
                   :exec 7th))
         (8th (mbe :logic (tree-list-fix 8th)
                   :exec 8th))
         (9th (mbe :logic (tree-list-fix 9th)
                   :exec 9th)))
      (list (cons '1st 1st)
            (cons '2nd 2nd)
            (cons '3rd 3rd)
            (cons '4th 4th)
            (cons '5th 5th)
            (cons '6th 6th)
            (cons '7th 7th)
            (cons '8th 8th)
            (cons '9th 9th)))))