		Search-engine friendly clone of the ACL2 documentation.

Vl-lexstate-p

Make-honsed-vl-lexstate

Constructor macro for honsed vl-lexstate-p structures.

Syntax:

(make-honsed-vl-lexstate [:kwdtable <kwdtable>] 
                         [:bangops <bangops>] 
                         [:poundops <poundops>] 
                         [:remops <remops>] 
                         [:andops <andops>] 
                         [:starops <starops>] 
                         [:plusops <plusops>] 
                         [:dashops <dashops>] 
                         [:dotops <dotops>] 
                         [:divops <divops>] 
                         [:colonops <colonops>] 
                         [:lessops <lessops>] 
                         [:gtops <gtops>] 
                         [:eqops <eqops>] 
                         [:xorops <xorops>] 
                         [:barops <barops>] 
                         [:dollarops <dollarops>] 
                         [:quotesp <quotesp>] 
                         [:strextsp <strextsp>] 
                         [:timelitsp <timelitsp>] 
                         [:extintsp <extintsp>] 
                         [:onestepp <onestepp>])

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

Definition

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

Macro: make-honsed-vl-lexstate

(defmacro make-honsed-vl-lexstate (&rest args)
  (std::make-aggregate 'vl-lexstate
                       args
                       '((:kwdtable)
                         (:bangops)
                         (:poundops)
                         (:remops)
                         (:andops)
                         (:starops)
                         (:plusops)
                         (:dashops)
                         (:dotops)
                         (:divops)
                         (:colonops)
                         (:lessops)
                         (:gtops)
                         (:eqops)
                         (:xorops)
                         (:barops)
                         (:dollarops)
                         (:quotesp)
                         (:strextsp)
                         (:timelitsp)
                         (:extintsp)
                         (:onestepp))
                       'make-honsed-vl-lexstate
                       t))