		Search-engine friendly clone of the ACL2 documentation.

Array-fieldinfo-p

Make-array-fieldinfo

Constructor macro for array-fieldinfo-p structures.

Syntax:

(make-array-fieldinfo [:tr-key <tr-key>] 
                      [:size-key <size-key>])

This is our preferred way to construct array-fieldinfo-p structures. It simply conses together a structure with the specified fields.

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

The array-fieldinfo-p structures we create here are just constructed with ordinary cons. If you want to create honsed structures, see make-honsed-array-fieldinfo instead.

Definition

This is an ordinary make- macro introduced by std::defaggregate.

Macro: make-array-fieldinfo

(defmacro make-array-fieldinfo (&rest args)
  (std::make-aggregate 'array-fieldinfo
                       args '((:tr-key) (:size-key))
                       'make-array-fieldinfo
                       nil))