		Search-engine friendly clone of the ACL2 documentation.

Vl-sysidtoken-p

Make-honsed-vl-sysidtoken

Constructor macro for honsed vl-sysidtoken-p structures.

Syntax:

(make-honsed-vl-sysidtoken [:etext <etext>] 
                           [:name <name>] 
                           [:breakp <breakp>])

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

Definition

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

Macro: make-honsed-vl-sysidtoken

(defmacro make-honsed-vl-sysidtoken (&rest args)
  (std::make-aggregate 'vl-sysidtoken
                       args '((:etext) (:name) (:breakp))
                       'make-honsed-vl-sysidtoken
                       t))