		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?>])

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?))
                       'make-initdeclor
                       nil))

Function: initdeclor

(defun initdeclor (declor asm? attribs init?)
  (declare (xargs :guard (and (declorp declor)
                              (asm-name-spec-optionp asm?)
                              (attrib-spec-listp attribs)
                              (initer-optionp init?))))
  (declare (xargs :guard t))
  (let ((__function__ 'initdeclor))
    (declare (ignorable __function__))
    (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?)))
      (list (cons 'declor declor)
            (cons 'asm? asm?)
            (cons 'attribs attribs)
            (cons 'init? init?)))))