		Search-engine friendly clone of the ACL2 documentation.

Lex-numbers

Vl-lex-unbased-unsized-literal

unbased_unsized_literal ::= '0 | '1 | 'z_or_x.

Signature
(vl-lex-unbased-unsized-literal echars breakp) → (mv token? remainder)
Arguments: echars — Guard (vl-echarlist-p echars).; breakp — Guard (booleanp breakp).

Embedded spaces are not allowed.

Definitions and Theorems

Function: vl-lex-unbased-unsized-literal

(defun vl-lex-unbased-unsized-literal (echars breakp)
  (declare (xargs :guard (and (vl-echarlist-p echars)
                              (booleanp breakp))))
  (let ((__function__ 'vl-lex-unbased-unsized-literal))
    (declare (ignorable __function__))
    (b* ((breakp (and breakp t))
         ((mv prefix val remainder)
          (b* (((mv prefix remainder)
                (vl-read-literal "'0" echars))
               ((when prefix)
                (mv prefix :vl-0val remainder))
               ((mv prefix remainder)
                (vl-read-literal "'1" echars))
               ((when prefix)
                (mv prefix :vl-1val remainder))
               ((mv prefix remainder)
                (vl-read-some-literal '("'x" "'X")
                                      echars))
               ((when prefix)
                (mv prefix :vl-xval remainder))
               ((mv prefix remainder)
                (vl-read-some-literal '("'z" "'Z")
                                      echars))
               ((when prefix)
                (mv prefix :vl-zval remainder)))
            (mv nil nil echars)))
         ((when prefix)
          (mv (make-vl-extinttoken :etext prefix
                                   :value val
                                   :breakp breakp)
              remainder)))
      (mv nil echars))))

Theorem: vl-token-p-of-vl-lex-unbased-unsized-literal

(defthm vl-token-p-of-vl-lex-unbased-unsized-literal
 (implies
  (and (force (vl-echarlist-p echars)) t)
  (equal
       (vl-token-p
            (mv-nth 0
                    (vl-lex-unbased-unsized-literal echars breakp)))
       (if (mv-nth 0
                   (vl-lex-unbased-unsized-literal echars breakp))
           t
         nil))))

Theorem: true-listp-of-vl-lex-unbased-unsized-literal

(defthm true-listp-of-vl-lex-unbased-unsized-literal
 (equal
      (true-listp
           (mv-nth 1
                   (vl-lex-unbased-unsized-literal echars breakp)))
      (true-listp echars))
 :rule-classes
 ((:rewrite)
  (:type-prescription
   :corollary
   (implies
    (true-listp echars)
    (true-listp
        (mv-nth 1
                (vl-lex-unbased-unsized-literal echars breakp)))))))

Theorem: vl-echarlist-p-of-vl-lex-unbased-unsized-literal

(defthm vl-echarlist-p-of-vl-lex-unbased-unsized-literal
 (implies
  (force (vl-echarlist-p echars))
  (equal
       (vl-echarlist-p
            (mv-nth 1
                    (vl-lex-unbased-unsized-literal echars breakp)))
       t)))

Theorem: append-of-vl-lex-unbased-unsized-literal

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

Theorem: no-change-loser-of-vl-lex-unbased-unsized-literal

(defthm no-change-loser-of-vl-lex-unbased-unsized-literal
 (implies
      (not (mv-nth 0
                   (vl-lex-unbased-unsized-literal echars breakp)))
      (equal (mv-nth 1
                     (vl-lex-unbased-unsized-literal echars breakp))
             echars)))

Theorem: acl2-count-of-vl-lex-unbased-unsized-literal-weak

(defthm acl2-count-of-vl-lex-unbased-unsized-literal-weak
  (<= (acl2-count
           (mv-nth 1
                   (vl-lex-unbased-unsized-literal echars breakp)))
      (acl2-count echars))
  :rule-classes ((:rewrite) (:linear)))

Theorem: acl2-count-of-vl-lex-unbased-unsized-literal-strong

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

Subtopics

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