Build an alist associating any "bad" wires with any "good" wires that they may be typos for.
(typo-detect bad good) → alist
Function:
(defun typo-detect (bad good) (declare (xargs :guard (and (string-listp bad) (string-listp good)))) (let ((__function__ 'typo-detect)) (declare (ignorable __function__)) (typo-detect-aux bad (typo-partitioning-alist good))))
Theorem:
(defthm alistp-of-typo-detect (b* ((alist (typo-detect bad good))) (alistp alist)) :rule-classes :rewrite)
Theorem:
(defthm vl-string-keys-p-of-typo-detect (implies (force (string-listp bad)) (vl-string-keys-p (typo-detect bad good))))
Theorem:
(defthm vl-string-list-values-p-of-typo-detect (implies (force (string-listp good)) (vl-string-list-values-p (typo-detect bad good))))