		Search-engine friendly clone of the ACL2 documentation.

Vls-data-p

Vls-data

Raw constructor for vls-data-p structures.

Syntax:

(vls-data good 
          bad orig orig-descalist filemap defs)

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

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

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

Definition

This is an ordinary constructor function introduced by defaggregate.

Function: vls-data

(defun vls-data (good bad orig orig-descalist filemap defs)
 (declare (xargs :guard (and (vl-design-p good)
                             (vl-design-p bad)
                             (vl-design-p orig)
                             (vl-descalist-okp orig orig-descalist)
                             (vl-filemap-p filemap)
                             (vl-defines-p defs))))
 (cons
   :vls-data
   (cons (cons 'good good)
         (cons (cons 'bad bad)
               (cons (cons 'orig orig)
                     (cons (cons 'orig-descalist orig-descalist)
                           (cons (cons 'filemap filemap)
                                 (cons (cons 'defs defs) nil))))))))