		Search-engine friendly clone of the ACL2 documentation.

Vls-data-p

Make-honsed-vls-data

Constructor macro for honsed vls-data-p structures.

Syntax:

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

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

Definition

This is an ordinary honsing make- macro introduced by defaggregate.

Macro: make-honsed-vls-data

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