		Search-engine friendly clone of the ACL2 documentation.

Comp-stmt

Make-comp-stmt

Basic constructor macro for comp-stmt structures.

Syntax

(make-comp-stmt [:labels <labels>] 
                [:items <items>])

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

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

Definition

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

Macro: make-comp-stmt

(defmacro make-comp-stmt (&rest args)
  (std::make-aggregate 'comp-stmt
                       args '((:labels) (:items))
                       'make-comp-stmt
                       nil))

Function: comp-stmt

(defun comp-stmt (labels items)
  (declare (xargs :guard (and (ident-list-listp labels)
                              (block-item-listp items))))
  (declare (xargs :guard t))
  (b* ((labels (mbe :logic (ident-list-list-fix labels)
                    :exec labels))
       (items (mbe :logic (block-item-list-fix items)
                   :exec items)))
    (cons labels items)))