		Search-engine friendly clone of the ACL2 documentation.

Array-fieldinfo-p

Make-honsed-array-fieldinfo

Constructor macro for honsed array-fieldinfo-p structures.

Syntax:

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

This is identical to make-array-fieldinfo, except that we hons the structure we are creating.

Definition

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

Macro: make-honsed-array-fieldinfo

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