		Search-engine friendly clone of the ACL2 documentation.

Vl-translation-p

Make-vl-translation

Constructor macro for vl-translation-p structures.

Syntax:

(make-vl-translation [:good <good>] 
                     [:bad <bad>] 
                     [:orig <orig>] 
                     [:filemap <filemap>] 
                     [:defines <defines>])

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

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

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

Definition

This is an ordinary make- macro introduced by defaggregate.

Macro: make-vl-translation

(defmacro make-vl-translation (&rest args)
  (std::make-aggregate 'vl-translation
                       args
                       '((:good)
                         (:bad)
                         (:orig)
                         (:filemap)
                         (:defines))
                       'make-vl-translation
                       nil))