		Search-engine friendly clone of the ACL2 documentation.

Typo-detection

Vl-typo-first-mismatch

Given two same-length partitionings, return their first mismatch as a pair.

Signature
(vl-typo-first-mismatch x y) → *

Definitions and Theorems

Function: vl-typo-first-mismatch

(defun vl-typo-first-mismatch (x y)
  (declare (xargs :guard (same-lengthp x y)))
  (let ((__function__ 'vl-typo-first-mismatch))
    (declare (ignorable __function__))
    (cond ((atom x) nil)
          ((equal (car x) (car y))
           (vl-typo-first-mismatch (cdr x)
                                   (cdr y)))
          (t (cons (car x) (car y))))))

Theorem: character-list-p-of-vl-typo-first-mismatch-1

(defthm character-list-p-of-vl-typo-first-mismatch-1
  (implies (and (character-list-listp x)
                (character-list-listp y))
           (character-listp (car (vl-typo-first-mismatch x y)))))

Theorem: character-list-p-of-vl-typo-first-mismatch-2

(defthm character-list-p-of-vl-typo-first-mismatch-2
  (implies (and (character-list-listp x)
                (character-list-listp y))
           (character-listp (cdr (vl-typo-first-mismatch x y)))))