		Search-engine friendly clone of the ACL2 documentation.

Lex-numbers

Vl-read-real-tail

Match exp [sign] unsigned_number

Signature
(vl-read-real-tail echars) → (mv prefix? remainder)
Arguments: echars — Guard (vl-echarlist-p echars).

Definitions and Theorems

Function: vl-read-real-tail$inline

(defun vl-read-real-tail$inline (echars)
  (declare (xargs :guard (vl-echarlist-p echars)))
  (let ((__function__ 'vl-read-real-tail))
    (declare (ignorable __function__))
    (b* (((mv e rem)
          (vl-read-some-literal '("e" "E")
                                echars))
         ((unless e) (mv nil echars))
         ((mv sign rem)
          (vl-read-some-literal '("+" "-") rem))
         ((mv expt rem)
          (vl-read-unsigned-number rem))
         ((unless expt) (mv nil echars)))
      (mv (append e sign expt) rem))))

Theorem: prefix-of-vl-read-real-tail

(defthm prefix-of-vl-read-real-tail
 (and
   (true-listp (mv-nth 0 (vl-read-real-tail echars)))
   (implies (force (vl-echarlist-p echars))
            (vl-echarlist-p (mv-nth 0 (vl-read-real-tail echars)))))
 :rule-classes
 ((:rewrite)
  (:type-prescription
    :corollary (true-listp (mv-nth 0 (vl-read-real-tail echars))))))

Theorem: remainder-of-vl-read-real-tail

(defthm remainder-of-vl-read-real-tail
 (and
   (equal (true-listp (mv-nth 1 (vl-read-real-tail echars)))
          (true-listp echars))
   (implies (force (vl-echarlist-p echars))
            (vl-echarlist-p (mv-nth 1 (vl-read-real-tail echars)))))
 :rule-classes
 ((:rewrite)
  (:type-prescription
     :corollary
     (implies (true-listp echars)
              (true-listp (mv-nth 1 (vl-read-real-tail echars)))))))

Theorem: append-of-vl-read-real-tail

(defthm append-of-vl-read-real-tail
  (equal (append (mv-nth 0 (vl-read-real-tail echars))
                 (mv-nth 1 (vl-read-real-tail echars)))
         echars))

Theorem: no-change-loser-of-vl-read-real-tail

(defthm no-change-loser-of-vl-read-real-tail
  (implies (not (mv-nth 0 (vl-read-real-tail echars)))
           (equal (mv-nth 1 (vl-read-real-tail echars))
                  echars)))

Theorem: acl2-count-of-vl-read-real-tail-weak

(defthm acl2-count-of-vl-read-real-tail-weak
  (<= (acl2-count (mv-nth 1 (vl-read-real-tail echars)))
      (acl2-count echars))
  :rule-classes ((:rewrite) (:linear)))

Theorem: acl2-count-of-vl-read-real-tail-strong

(defthm acl2-count-of-vl-read-real-tail-strong
  (implies (mv-nth 0 (vl-read-real-tail echars))
           (< (acl2-count (mv-nth 1 (vl-read-real-tail echars)))
              (acl2-count echars)))
  :rule-classes ((:rewrite) (:linear)))

Subtopics

Vl-read-real-tail-prefix/remainder-thms: Prefix and remainder theorems for vl-read-real-tail, automatically generated by def-prefix/remainder-thms.