		Search-engine friendly clone of the ACL2 documentation.

Vl-translation-p

Vl-translation

Raw constructor for vl-translation-p structures.

Syntax:

(vl-translation good bad orig filemap defines)

This is the lowest-level constructor for vl-translation-p structures. It simply conses together a structure with the specified fields.

Note: It's generally better to use macros like make-vl-translation or change-vl-translation instead. These macros lead to more readable and robust code, because you don't have to remember the order of the fields.

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

Definition

This is an ordinary constructor function introduced by defaggregate.

Function: vl-translation

(defun vl-translation (good bad orig filemap defines)
 (declare (xargs :guard (and (vl-design-p good)
                             (vl-design-p bad)
                             (vl-design-p orig)
                             (vl-filemap-p filemap)
                             (vl-defines-p defines))))
 (cons
    :vl-translation
    (cons (cons 'good good)
          (cons (cons 'bad bad)
                (cons (cons 'orig orig)
                      (cons (cons 'filemap filemap)
                            (cons (cons 'defines defines) nil)))))))