		Search-engine friendly clone of the ACL2 documentation.

Vls-data-p

Vls-data

Raw constructor for vls-data-p structures.

Syntax:

(vls-data orig name 
          date ltime 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 (orig name
                      date ltime orig-descalist filemap defs)
 (declare (xargs :guard (and (vl-design-p orig)
                             (stringp name)
                             (stringp date)
                             (natp ltime)
                             (vl-descalist-okp orig orig-descalist)
                             (vl-filemap-p filemap)
                             (vl-defines-p defs))))
 (cons
  :vls-data
  (cons
   (cons 'orig orig)
   (cons
        (cons 'name name)
        (cons (cons 'date date)
              (cons (cons 'ltime ltime)
                    (cons (cons 'orig-descalist orig-descalist)
                          (cons (cons 'filemap filemap)
                                (cons (cons 'defs defs) nil)))))))))