		Search-engine friendly clone of the ACL2 documentation.

Initdeclor

Make-initdeclor

Basic constructor macro for initdeclor structures.

Syntax

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

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

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

Definition

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

Macro: make-initdeclor

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

Function: initdeclor

(defun initdeclor (declor asm? attribs init? info)
  (declare (xargs :guard (and (declorp declor)
                              (asm-name-spec-optionp asm?)
                              (attrib-spec-listp attribs)
                              (initer-optionp init?)
                              (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))
       (init? (mbe :logic (initer-option-fix init?)
                   :exec init?))
       (info (mbe :logic (identity info)
                  :exec info)))
    (cons (cons declor asm?)
          (cons attribs (cons init? info)))))