		Search-engine friendly clone of the ACL2 documentation.

Absdeclor

Make-absdeclor

Basic constructor macro for absdeclor structures.

Syntax

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

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) (:direct?))
                       'make-absdeclor
                       nil))

Function: absdeclor

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