(vl-lex-unbased-unsized-literal echars breakp) → (mv token? remainder)
Embedded spaces are not allowed.
Function:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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)))