		Search-engine friendly clone of the ACL2 documentation.

Lex-numbers

Vl-lex-number

Match number, time_literal, and unbased_unsized_literal.

Signature
(vl-lex-number echars breakp st warnings) → (mv token? remainder warnings)
Arguments: echars — Guard (vl-echarlist-p echars).; breakp — Guard (booleanp breakp).; st — Guard (vl-lexstate-p st).; warnings — Guard (vl-warninglist-p warnings).
Returns: warnings — Type (vl-warninglist-p warnings).

Definitions and Theorems

Function: vl-lex-number$inline

(defun vl-lex-number$inline (echars breakp st warnings)
  (declare (xargs :guard (and (vl-echarlist-p echars)
                              (booleanp breakp)
                              (vl-lexstate-p st)
                              (vl-warninglist-p warnings))))
  (let ((__function__ 'vl-lex-number))
    (declare (ignorable __function__))
    (b* ((warnings (vl-warninglist-fix warnings))
         ((mv token remainder)
          (vl-lex-time-or-real-number echars breakp st))
         ((when token)
          (mv token remainder warnings))
         ((mv token remainder warnings)
          (vl-lex-integer echars breakp warnings))
         ((when token)
          (mv token remainder warnings))
         ((unless (vl-lexstate->extintsp st))
          (mv nil echars warnings))
         ((mv token remainder)
          (vl-lex-unbased-unsized-literal echars breakp)))
      (mv token remainder warnings))))

Theorem: vl-warninglist-p-of-vl-lex-number.warnings

(defthm vl-warninglist-p-of-vl-lex-number.warnings
  (b* (((mv ?token? ?remainder ?warnings)
        (vl-lex-number$inline echars breakp st warnings)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-token-p-of-vl-lex-number

(defthm vl-token-p-of-vl-lex-number
 (implies
  (and (force (vl-echarlist-p echars)) t)
  (equal
     (vl-token-p (mv-nth 0
                         (vl-lex-number echars breakp st warnings)))
     (if (mv-nth 0
                 (vl-lex-number echars breakp st warnings))
         t
       nil))))

Theorem: true-listp-of-vl-lex-number

(defthm true-listp-of-vl-lex-number
 (equal
     (true-listp (mv-nth 1
                         (vl-lex-number echars breakp st warnings)))
     (true-listp echars))
 :rule-classes
 ((:rewrite)
  (:type-prescription
   :corollary
   (implies
        (true-listp echars)
        (true-listp
             (mv-nth 1
                     (vl-lex-number echars breakp st warnings)))))))

Theorem: vl-echarlist-p-of-vl-lex-number

(defthm vl-echarlist-p-of-vl-lex-number
 (implies
     (force (vl-echarlist-p echars))
     (equal (vl-echarlist-p
                 (mv-nth 1
                         (vl-lex-number echars breakp st warnings)))
            t)))

Theorem: append-of-vl-lex-number

(defthm append-of-vl-lex-number
 (implies
  (and (mv-nth 0
               (vl-lex-number echars breakp st warnings))
       (force (vl-echarlist-p echars))
       t)
  (equal
    (append (vl-token->etext
                 (mv-nth 0
                         (vl-lex-number echars breakp st warnings)))
            (mv-nth 1
                    (vl-lex-number echars breakp st warnings)))
    echars)))

Theorem: no-change-loser-of-vl-lex-number

(defthm no-change-loser-of-vl-lex-number
  (implies (not (mv-nth 0
                        (vl-lex-number echars breakp st warnings)))
           (equal (mv-nth 1
                          (vl-lex-number echars breakp st warnings))
                  echars)))

Theorem: acl2-count-of-vl-lex-number-weak

(defthm acl2-count-of-vl-lex-number-weak
 (<= (acl2-count (mv-nth 1
                         (vl-lex-number echars breakp st warnings)))
     (acl2-count echars))
 :rule-classes ((:rewrite) (:linear)))

Theorem: acl2-count-of-vl-lex-number-strong

(defthm acl2-count-of-vl-lex-number-strong
 (implies
  (and (mv-nth 0
               (vl-lex-number echars breakp st warnings))
       t)
  (< (acl2-count (mv-nth 1
                         (vl-lex-number echars breakp st warnings)))
     (acl2-count echars)))
 :rule-classes ((:rewrite) (:linear)))

Subtopics

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