		Search-engine friendly clone of the ACL2 documentation.

Block-item-declon

Make-block-item-declon

Basic constructor macro for block-item-declon structures.

Syntax

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

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

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

Definition

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

Macro: make-block-item-declon

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

Function: block-item-declon

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