Given two same-length partitionings, return their first mismatch as a pair.
(vl-typo-first-mismatch x y) → *
Function:
(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:
(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:
(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)))))