		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) → (mv token? remainder)
Arguments: echars — Guard (vl-echarlist-p echars).

Embedded spaces are not allowed.

Definitions and Theorems

Function: vl-lex-unbased-unsized-literal

(defun vl-lex-unbased-unsized-literal (echars)
  (declare (xargs :guard (vl-echarlist-p echars)))
  (let ((__function__ 'vl-lex-unbased-unsized-literal))
    (declare (ignorable __function__))
    (b* (((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)
              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)))
       (if (mv-nth 0
                   (vl-lex-unbased-unsized-literal echars))
           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)))
      (true-listp echars))
 :rule-classes
 ((:rewrite)
  (:type-prescription
     :corollary
     (implies
          (true-listp echars)
          (true-listp
               (mv-nth 1
                       (vl-lex-unbased-unsized-literal echars)))))))

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)))
   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))
       (force (vl-echarlist-p echars))
       t)
  (equal
      (append (vl-token->etext
                   (mv-nth 0
                           (vl-lex-unbased-unsized-literal echars)))
              (mv-nth 1
                      (vl-lex-unbased-unsized-literal echars)))
      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)))
           (equal (mv-nth 1
                          (vl-lex-unbased-unsized-literal echars))
                  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)))
      (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))
         t)
    (< (acl2-count (mv-nth 1
                           (vl-lex-unbased-unsized-literal echars)))
       (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.