		Search-engine friendly clone of the ACL2 documentation.

Vls-data-p

Honsed-vls-data

Raw constructor for honsed vls-data-p structures.

Syntax:

(honsed-vls-data orig name 
                 date ltime orig-descalist filemap defs)

This is identical to vls-data, except that we hons the structure we are creating.

Definition

This is an ordinary honsing constructor introduced by defaggregate.

Function: honsed-vls-data

(defun honsed-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))))
 (mbe
  :logic (vls-data orig name
                   date ltime orig-descalist filemap defs)
  :exec
  (hons
   :vls-data
   (hons
    (hons 'orig orig)
    (hons
       (hons 'name name)
       (hons (hons 'date date)
             (hons (hons 'ltime ltime)
                   (hons (hons 'orig-descalist orig-descalist)
                         (hons (hons 'filemap filemap)
                               (hons (hons 'defs defs) nil))))))))))