		Search-engine friendly clone of the ACL2 documentation.

Transunit-ensemble

Make-transunit-ensemble

Basic constructor macro for transunit-ensemble structures.

Syntax

(make-transunit-ensemble [:units <units>])

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

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

Definition

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

Macro: make-transunit-ensemble

(defmacro make-transunit-ensemble (&rest args)
  (std::make-aggregate 'transunit-ensemble
                       args '((:units))
                       'make-transunit-ensemble
                       nil))

Function: transunit-ensemble

(defun transunit-ensemble (units)
  (declare (xargs :guard (filepath-transunit-mapp units)))
  (declare (xargs :guard t))
  (b* ((units (mbe :logic (filepath-transunit-map-fix units)
                   :exec units)))
    units))