		Search-engine friendly clone of the ACL2 documentation.

Vls-data-p

Make-vls-data

Constructor macro for vls-data-p structures.

Syntax:

(make-vls-data [:orig <orig>] 
               [:name <name>] 
               [:date <date>] 
               [:ltime <ltime>] 
               [:orig-descalist <orig-descalist>] 
               [:filemap <filemap>] 
               [:defs <defs>])

This is our preferred way to construct vls-data-p structures. It simply conses together a structure with the specified fields.

This macro generates a new vls-data-p structure from scratch. See also change-vls-data, which can "change" an existing structure, instead.

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

Definition

This is an ordinary make- macro introduced by defaggregate.

Macro: make-vls-data

(defmacro make-vls-data (&rest args)
  (std::make-aggregate 'vls-data
                       args
                       '((:orig)
                         (:name)
                         (:date)
                         (:ltime)
                         (:orig-descalist)
                         (:filemap)
                         (:defs))
                       'make-vls-data
                       nil))