		Search-engine friendly clone of the ACL2 documentation.

Stvdata-p

Make-stvdata

Constructor macro for stvdata-p structures.

Syntax:

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

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

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

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

Definition

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

Macro: make-stvdata

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