		Search-engine friendly clone of the ACL2 documentation.

Absdeclor

Make-absdeclor

Basic constructor macro for absdeclor structures.

Syntax

(make-absdeclor [:pointers <pointers>] 
                [:decl? <decl?>])

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

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

Definition

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

Macro: make-absdeclor

(defmacro make-absdeclor (&rest args)
  (std::make-aggregate 'absdeclor
                       args '((:pointers) (:decl?))
                       'make-absdeclor
                       nil))

Function: absdeclor

(defun absdeclor (pointers decl?)
 (declare
      (xargs :guard (and (typequal/attribspec-list-listp pointers)
                         (dirabsdeclor-optionp decl?))))
 (declare (xargs :guard t))
 (let ((__function__ 'absdeclor))
  (declare (ignorable __function__))
  (b* ((pointers
            (mbe :logic (typequal/attribspec-list-list-fix pointers)
                 :exec pointers))
       (decl? (mbe :logic (dirabsdeclor-option-fix decl?)
                   :exec decl?)))
    (list (cons 'pointers pointers)
          (cons 'decl? decl?)))))