		Search-engine friendly clone of the ACL2 documentation.

Stvdata-p

Make-honsed-stvdata

Constructor macro for honsed stvdata-p structures.

Syntax:

(make-honsed-stvdata [:inputs <inputs>] 
                     [:outputs <outputs>] 
                     [:internals <internals>] 
                     [:overrides <overrides>])

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

Definition

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

Macro: make-honsed-stvdata

(defmacro make-honsed-stvdata (&rest args)
          (std::make-aggregate 'stvdata
                               args
                               '((:inputs)
                                 (:outputs)
                                 (:internals)
                                 (:overrides))
                               'make-honsed-stvdata
                               t))