		Search-engine friendly clone of the ACL2 documentation.

Declon/stmt-declon

Make-declon/stmt-declon

Basic constructor macro for declon/stmt-declon structures.

Syntax

(make-declon/stmt-declon [:declon <declon>])

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

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

Definition

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

Macro: make-declon/stmt-declon

(defmacro make-declon/stmt-declon (&rest args)
  (std::make-aggregate 'declon/stmt-declon
                       args '((:declon))
                       'make-declon/stmt-declon
                       nil))

Function: declon/stmt-declon

(defun declon/stmt-declon (declon)
  (declare (xargs :guard (declonp declon)))
  (declare (xargs :guard t))
  (b* ((declon (mbe :logic (declon-fix declon)
                    :exec declon)))
    (cons :declon declon)))