		Search-engine friendly clone of the ACL2 documentation.

Lexstate

Vl-lexstate-init

User-level constructor for internal lexer states.

Signature
(vl-lexstate-init config) → st
Arguments: config — Guard (vl-loadconfig-p config).
Returns: st — Type (vl-lexstate-p st).

Definitions and Theorems

Function: vl-lexstate-init

(defun vl-lexstate-init (config)
 (declare (xargs :guard (vl-loadconfig-p config)))
 (let ((__function__ 'vl-lexstate-init))
  (declare (ignorable __function__))
  (b* (((vl-loadconfig config) config))
   (case config.edition
         (:verilog-2005 (if config.strictp *vl-2005-strict-lexstate*
                          *vl-2005-lexstate*))
         (:system-verilog-2012
              (if config.strictp *vl-2012-strict-lexstate*
                *vl-2012-lexstate*))
         (otherwise (progn$ (impossible)
                            *vl-2012-lexstate*))))))

Theorem: vl-lexstate-p-of-vl-lexstate-init

(defthm vl-lexstate-p-of-vl-lexstate-init
  (b* ((st (vl-lexstate-init config)))
    (vl-lexstate-p st))
  :rule-classes :rewrite)