		Search-engine friendly clone of the ACL2 documentation.

Output-section

Make-output-section

Basic constructor macro for output-section structures.

Syntax

(make-output-section [:item <item>])

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

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

Definition

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

Macro: make-output-section

(defmacro make-output-section (&rest args)
  (std::make-aggregate 'output-section
                       args '((:item))
                       'make-output-section
                       nil))

Function: output-section

(defun output-section (item)
  (declare (xargs :guard (output-itemp item)))
  (declare (xargs :guard t))
  (let ((__function__ 'output-section))
    (declare (ignorable __function__))
    (b* ((item (mbe :logic (output-item-fix item)
                    :exec item)))
      (cons :output-section (list (cons 'item item))))))