		Search-engine friendly clone of the ACL2 documentation.

Ext-declon-declon

Make-ext-declon-declon

Basic constructor macro for ext-declon-declon structures.

Syntax

(make-ext-declon-declon [:declon <declon>])

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

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

Definition

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

Macro: make-ext-declon-declon

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

Function: ext-declon-declon

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