		Search-engine friendly clone of the ACL2 documentation.

Typo-detection

Typo-partition

Fully partition a wire name.

Signature
(typo-partition x) → parts
Arguments: x — Guard (character-listp x).
Returns: parts — Type (character-list-listp parts), given the guard.

Definitions and Theorems

Function: typo-partition

(defun typo-partition (x)
  (declare (xargs :guard (character-listp x)))
  (let ((__function__ 'typo-partition))
    (declare (ignorable __function__))
    (b* (((when (atom x)) nil)
         ((mv prefix remainder)
          (typo-read-part x))
         ((unless prefix) nil))
      (cons prefix (typo-partition remainder)))))

Theorem: character-list-listp-of-typo-partition

(defthm character-list-listp-of-typo-partition
  (implies (and (force (character-listp x)))
           (b* ((parts (typo-partition x)))
             (character-list-listp parts)))
  :rule-classes :rewrite)

Theorem: true-listp-of-typo-partition

(defthm true-listp-of-typo-partition
  (true-listp (typo-partition x))
  :rule-classes :type-prescription)