		Search-engine friendly clone of the ACL2 documentation.

Token-p

Make-token

Constructor macro for token-p structures.

Syntax:

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

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

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

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

Definition

This is an ordinary make- macro introduced by defaggregate.

Macro: make-token

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