		Search-engine friendly clone of the ACL2 documentation.

Typo-detection

Typo-read-lowercase-part

Read as many lowercase characters as possible, but stop early if a special is encountered.

Signature
(typo-read-lowercase-part x) → (mv prefix remainder)
Arguments: x — Guard (character-listp x).
Returns: prefix — Type (character-listp prefix), given (force (character-listp x)).; remainder — Type (character-listp remainder), given (force (character-listp x)).

Definitions and Theorems

Function: typo-read-lowercase-part

(defun typo-read-lowercase-part (x)
  (declare (xargs :guard (character-listp x)))
  (let ((__function__ 'typo-read-lowercase-part))
    (declare (ignorable __function__))
    (b* (((when (atom x)) (mv nil x))
         ((mv prefix ?remainder)
          (typo-read-special *typo-special-substrings-chars* x))
         ((when prefix) (mv nil x))
         ((unless (vl-typo-lowercase-p (car x)))
          (mv nil x))
         ((mv prefix remainder)
          (typo-read-lowercase-part (cdr x))))
      (mv (cons (car x) prefix) remainder))))

Theorem: character-listp-of-typo-read-lowercase-part.prefix

(defthm character-listp-of-typo-read-lowercase-part.prefix
  (implies (force (character-listp x))
           (b* (((mv ?prefix ?remainder)
                 (typo-read-lowercase-part x)))
             (character-listp prefix)))
  :rule-classes :rewrite)

Theorem: character-listp-of-typo-read-lowercase-part.remainder

(defthm character-listp-of-typo-read-lowercase-part.remainder
  (implies (force (character-listp x))
           (b* (((mv ?prefix ?remainder)
                 (typo-read-lowercase-part x)))
             (character-listp remainder)))
  :rule-classes :rewrite)

Theorem: true-listp-of-typo-read-lowercase-part

(defthm true-listp-of-typo-read-lowercase-part
  (true-listp (mv-nth 0 (typo-read-lowercase-part x)))
  :rule-classes :type-prescription)

Theorem: typo-read-lowercase-car-under-iff

(defthm typo-read-lowercase-car-under-iff
 (implies
  (not
     (mv-nth 0
             (typo-read-special *typo-special-substrings-chars* x)))
  (iff (mv-nth 0 (typo-read-lowercase-part x))
       (vl-typo-lowercase-p (car x)))))

Theorem: acl2-count-of-typo-read-lowercase-weak

(defthm acl2-count-of-typo-read-lowercase-weak
  (<= (acl2-count (mv-nth 1 (typo-read-lowercase-part x)))
      (acl2-count x))
  :rule-classes ((:rewrite) (:linear)))

Theorem: acl2-count-of-typo-read-lowercase-strong

(defthm acl2-count-of-typo-read-lowercase-strong
  (implies (mv-nth 0 (typo-read-lowercase-part x))
           (< (acl2-count (mv-nth 1 (typo-read-lowercase-part x)))
              (acl2-count x)))
  :rule-classes ((:rewrite) (:linear)))