		Search-engine friendly clone of the ACL2 documentation.

Token-p

Make-honsed-token

Constructor macro for honsed token-p structures.

Syntax:

(make-honsed-token [:type <type>] 
                   [:text <text>])

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

Definition

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

Macro: make-honsed-token

(defmacro make-honsed-token (&rest args)
  (std::make-aggregate 'token
                       args '((:type) (:text))
                       'make-honsed-token
                       t))