		Search-engine friendly clone of the ACL2 documentation.

Svexl

Make-svexl

Basic constructor macro for svexl structures.

Syntax

(make-svexl [:top-node <top-node>] 
            [:node-array <node-array>])

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

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

Definition

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

Macro: make-svexl

(defmacro make-svexl (&rest args)
  (std::make-aggregate 'svexl
                       args '((:top-node) (:node-array))
                       'make-svexl
                       nil))

Function: svexl

(defun svexl (top-node node-array)
  (declare (xargs :guard (and (svexl-node-p top-node)
                              (svexl-node-array-p node-array))))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'svexl))
    (declare (ignorable acl2::__function__))
    (b* ((top-node (mbe :logic (svexl-node-fix top-node)
                        :exec top-node))
         (node-array (mbe :logic (svexl-node-array-fix node-array)
                          :exec node-array)))
      (list (cons 'top-node top-node)
            (cons 'node-array node-array)))))