		Search-engine friendly clone of the ACL2 documentation.

Declor

Make-declor

Basic constructor macro for declor structures.

Syntax

(make-declor [:pointers <pointers>] 
             [:direct <direct>])

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

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

Definition

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

Macro: make-declor

(defmacro make-declor (&rest args)
  (std::make-aggregate 'declor
                       args '((:pointers) (:direct))
                       'make-declor
                       nil))

Function: declor

(defun declor (pointers direct)
 (declare
      (xargs :guard (and (typequal/attribspec-list-listp pointers)
                         (dirdeclorp direct))))
 (declare (xargs :guard t))
 (let ((__function__ 'declor))
  (declare (ignorable __function__))
  (b* ((pointers
            (mbe :logic (typequal/attribspec-list-list-fix pointers)
                 :exec pointers))
       (direct (mbe :logic (dirdeclor-fix direct)
                    :exec direct)))
    (list (cons 'pointers pointers)
          (cons 'direct direct)))))