		Search-engine friendly clone of the ACL2 documentation.

Typo-detection

Typo-detect

Build an alist associating any "bad" wires with any "good" wires that they may be typos for.

Signature
(typo-detect bad good) → alist
Arguments: bad — Names of wires we think are somehow bad. It could be, e.g., all of the implicit wires in a module, or all of the implicit wires that are only partly used, etc.
Guard (string-listp bad).; good — Names of all the wires we think are somehow good; e.g., declared, used, etc.
Guard (string-listp good).
Returns: alist — Type (alistp alist).

Definitions and Theorems

Function: typo-detect

(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: alistp-of-typo-detect

(defthm alistp-of-typo-detect
  (b* ((alist (typo-detect bad good)))
    (alistp alist))
  :rule-classes :rewrite)

Theorem: vl-string-keys-p-of-typo-detect

(defthm vl-string-keys-p-of-typo-detect
  (implies (force (string-listp bad))
           (vl-string-keys-p (typo-detect bad good))))

Theorem: vl-string-list-values-p-of-typo-detect

(defthm vl-string-list-values-p-of-typo-detect
  (implies (force (string-listp good))
           (vl-string-list-values-p (typo-detect bad good))))