		Search-engine friendly clone of the ACL2 documentation.

Declon-declon

Make-declon-declon

Basic constructor macro for declon-declon structures.

Syntax

(make-declon-declon [:extension <extension>] 
                    [:specs <specs>] 
                    [:declors <declors>])

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

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

Definition

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

Macro: make-declon-declon

(defmacro make-declon-declon (&rest args)
  (std::make-aggregate 'declon-declon
                       args '((:extension) (:specs) (:declors))
                       'make-declon-declon
                       nil))

Function: declon-declon

(defun declon-declon (extension specs declors)
  (declare (xargs :guard (and (booleanp extension)
                              (decl-spec-listp specs)
                              (init-declor-listp declors))))
  (declare (xargs :guard t))
  (b* ((extension (mbe :logic (bool-fix extension)
                       :exec extension))
       (specs (mbe :logic (decl-spec-list-fix specs)
                   :exec specs))
       (declors (mbe :logic (init-declor-list-fix declors)
                     :exec declors)))
    (cons :declon (cons extension (cons specs declors)))))