		Search-engine friendly clone of the ACL2 documentation.

Init-declor

Make-init-declor

Basic constructor macro for init-declor structures.

Syntax

(make-init-declor [:declor <declor>] 
                  [:asm? <asm?>] 
                  [:attribs <attribs>] 
                  [:initer? <initer?>] 
                  [:info <info>])

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

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

Definition

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

Macro: make-init-declor

(defmacro make-init-declor (&rest args)
  (std::make-aggregate 'init-declor
                       args
                       '((:declor)
                         (:asm?)
                         (:attribs)
                         (:initer?)
                         (:info))
                       'make-init-declor
                       nil))

Function: init-declor

(defun init-declor (declor asm? attribs initer? info)
  (declare (xargs :guard (and (declorp declor)
                              (asm-name-spec-optionp asm?)
                              (attrib-spec-listp attribs)
                              (initer-optionp initer?)
                              (acl2::any-p info))))
  (declare (xargs :guard t))
  (b* ((declor (mbe :logic (declor-fix declor)
                    :exec declor))
       (asm? (mbe :logic (asm-name-spec-option-fix asm?)
                  :exec asm?))
       (attribs (mbe :logic (attrib-spec-list-fix attribs)
                     :exec attribs))
       (initer? (mbe :logic (initer-option-fix initer?)
                     :exec initer?))
       (info (mbe :logic (identity info)
                  :exec info)))
    (cons (cons declor asm?)
          (cons attribs (cons initer? info)))))