		Search-engine friendly clone of the ACL2 documentation.

Code-ensemble

Make-code-ensemble

Basic constructor macro for code-ensemble structures.

Syntax

(make-code-ensemble [:transunits <transunits>] 
                    [:ienv <ienv>])

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

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

Definition

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

Macro: make-code-ensemble

(defmacro make-code-ensemble (&rest args)
  (std::make-aggregate 'code-ensemble
                       args '((:transunits) (:ienv))
                       'make-code-ensemble
                       nil))

Function: code-ensemble

(defun code-ensemble (transunits ienv)
  (declare (xargs :guard (and (transunit-ensemblep transunits)
                              (ienvp ienv))))
  (declare (xargs :guard t))
  (b* ((transunits (mbe :logic (transunit-ensemble-fix transunits)
                        :exec transunits))
       (ienv (mbe :logic (c::ienv-fix ienv)
                  :exec ienv)))
    (list (cons 'transunits transunits)
          (cons 'ienv ienv))))