		Search-engine friendly clone of the ACL2 documentation.

Block-item-decl

Make-block-item-decl

Basic constructor macro for block-item-decl structures.

Syntax

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

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

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

Definition

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

Macro: make-block-item-decl

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

Function: block-item-decl

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