		Search-engine friendly clone of the ACL2 documentation.

Lex-comments

Vl-lex-oneline-comment

Try to match a // ... style comment.

Signature
(vl-lex-oneline-comment echars) → (mv token/nil remainder)
Arguments: echars — Guard (vl-echarlist-p echars).

Definitions and Theorems

Function: vl-lex-oneline-comment

(defun vl-lex-oneline-comment (echars)
  (declare (xargs :guard (vl-echarlist-p echars)))
  (let ((__function__ 'vl-lex-oneline-comment))
    (declare (ignorable __function__))
    (b* (((unless (vl-matches-string-p "//" echars))
          (mv nil echars))
         ((mv & prefix remainder)
          (vl-read-through-literal *nls* (cddr echars)))
         (etext (list* (first echars)
                       (second echars)
                       prefix))
         (token (make-vl-plaintoken :etext etext
                                    :type :vl-comment)))
      (mv token remainder))))

Subtopics

Vl-lex-oneline-comment-token/remainder-thms: Token and remainder theorems for vl-lex-oneline-comment, automatically generated by def-token/remainder-thms.