		Search-engine friendly clone of the ACL2 documentation.

Vl-lexstate-p

Vl-lexstate

Raw constructor for vl-lexstate-p structures.

Syntax:

(vl-lexstate kwdtable bangops 
             poundops remops andops starops plusops 
             dashops dotops divops colonops lessops 
             gtops eqops xorops barops dollarops 
             quotesp strextsp timelitsp extintsp)

This is the lowest-level constructor for vl-lexstate-p structures. It simply conses together a structure with the specified fields.

Note: It's generally better to use macros like make-vl-lexstate or change-vl-lexstate instead. These macros lead to more readable and robust code, because you don't have to remember the order of the fields.

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

Definition

This is an ordinary constructor function introduced by defaggregate.

Function: vl-lexstate

(defun vl-lexstate (kwdtable bangops
                             poundops remops andops starops plusops
                             dashops dotops divops colonops lessops
                             gtops eqops xorops barops dollarops
                             quotesp strextsp timelitsp extintsp)
  (declare (xargs :guard (and (vl-keyword-table-p kwdtable)
                              (vl-plaintoken-alistp bangops)
                              (vl-plaintoken-alistp poundops)
                              (vl-plaintoken-alistp remops)
                              (vl-plaintoken-alistp andops)
                              (vl-plaintoken-alistp starops)
                              (vl-plaintoken-alistp plusops)
                              (vl-plaintoken-alistp dashops)
                              (vl-plaintoken-alistp dotops)
                              (vl-plaintoken-alistp divops)
                              (vl-plaintoken-alistp colonops)
                              (vl-plaintoken-alistp lessops)
                              (vl-plaintoken-alistp gtops)
                              (vl-plaintoken-alistp eqops)
                              (vl-plaintoken-alistp xorops)
                              (vl-plaintoken-alistp barops)
                              (vl-plaintoken-alistp dollarops)
                              (booleanp quotesp)
                              (booleanp strextsp)
                              (booleanp timelitsp)
                              (booleanp extintsp))))
  (cons (cons (cons (cons kwdtable bangops)
                    (cons poundops (cons remops andops)))
              (cons (cons starops plusops)
                    (cons dashops (cons dotops divops))))
        (cons (cons (cons colonops lessops)
                    (cons gtops (cons eqops xorops)))
              (cons (cons barops (cons dollarops quotesp))
                    (cons strextsp (cons timelitsp extintsp))))))