		Search-engine friendly clone of the ACL2 documentation.

Vl-translation-p

Honsed-vl-translation

Raw constructor for honsed vl-translation-p structures.

Syntax:

(honsed-vl-translation good bad orig filemap defines)

This is identical to vl-translation, except that we hons the structure we are creating.

Definition

This is an ordinary honsing constructor introduced by defaggregate.

Function: honsed-vl-translation

(defun honsed-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))))
 (mbe
   :logic (vl-translation good bad orig filemap defines)
   :exec (hons :vl-translation
               (hons (hons 'good good)
                     (hons (hons 'bad bad)
                           (hons (hons 'orig orig)
                                 (hons (hons 'filemap filemap)
                                       (hons (hons 'defines defines)
                                             nil))))))))