		Search-engine friendly clone of the ACL2 documentation.

Block-item-stmt

Make-block-item-stmt

Basic constructor macro for block-item-stmt structures.

Syntax

(make-block-item-stmt [:stmt <stmt>] 
                      [:info <info>])

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

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

Definition

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

Macro: make-block-item-stmt

(defmacro make-block-item-stmt (&rest args)
  (std::make-aggregate 'block-item-stmt
                       args '((:stmt) (:info))
                       'make-block-item-stmt
                       nil))

Function: block-item-stmt

(defun block-item-stmt (stmt info)
  (declare (xargs :guard (and (stmtp stmt) (acl2::any-p info))))
  (declare (xargs :guard t))
  (b* ((stmt (mbe :logic (stmt-fix stmt) :exec stmt))
       (info (mbe :logic (identity info)
                  :exec info)))
    (cons :stmt (cons stmt info))))