		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-lucid-typo-detect

Signature
(vl-lucid-typo-detect candidates reportcard) → reportcard
Arguments: candidates — Already cleaned so we can recur through them.
Guard (vl-typocandidates-p candidates).; reportcard — So we can attach any real warnings.
Guard (vl-reportcard-p reportcard).
Returns: reportcard — Type (vl-reportcard-p reportcard).

Definitions and Theorems

Function: vl-lucid-typo-detect

(defun vl-lucid-typo-detect (candidates reportcard)
  (declare (xargs :guard (and (vl-typocandidates-p candidates)
                              (vl-reportcard-p reportcard))))
  (let ((__function__ 'vl-lucid-typo-detect))
    (declare (ignorable __function__))
    (b* ((candidates (vl-typocandidates-fix candidates))
         ((when (atom candidates))
          (vl-reportcard-fix reportcard))
         ((cons ss possible-typos)
          (car candidates))
         (reportcard
              (vl-lucid-typo-detect1 ss possible-typos reportcard)))
      (vl-lucid-typo-detect (cdr candidates)
                            reportcard))))

Theorem: vl-reportcard-p-of-vl-lucid-typo-detect

(defthm vl-reportcard-p-of-vl-lucid-typo-detect
  (b* ((reportcard (vl-lucid-typo-detect candidates reportcard)))
    (vl-reportcard-p reportcard))
  :rule-classes :rewrite)

Theorem: vl-lucid-typo-detect-of-vl-typocandidates-fix-candidates

(defthm vl-lucid-typo-detect-of-vl-typocandidates-fix-candidates
  (equal (vl-lucid-typo-detect (vl-typocandidates-fix candidates)
                               reportcard)
         (vl-lucid-typo-detect candidates reportcard)))

Theorem: vl-lucid-typo-detect-vl-typocandidates-equiv-congruence-on-candidates

(defthm
 vl-lucid-typo-detect-vl-typocandidates-equiv-congruence-on-candidates
 (implies
      (vl-typocandidates-equiv candidates candidates-equiv)
      (equal (vl-lucid-typo-detect candidates reportcard)
             (vl-lucid-typo-detect candidates-equiv reportcard)))
 :rule-classes :congruence)

Theorem: vl-lucid-typo-detect-of-vl-reportcard-fix-reportcard

(defthm vl-lucid-typo-detect-of-vl-reportcard-fix-reportcard
  (equal (vl-lucid-typo-detect candidates
                               (vl-reportcard-fix reportcard))
         (vl-lucid-typo-detect candidates reportcard)))

Theorem: vl-lucid-typo-detect-vl-reportcard-equiv-congruence-on-reportcard

(defthm
  vl-lucid-typo-detect-vl-reportcard-equiv-congruence-on-reportcard
  (implies
       (vl-reportcard-equiv reportcard reportcard-equiv)
       (equal (vl-lucid-typo-detect candidates reportcard)
              (vl-lucid-typo-detect candidates reportcard-equiv)))
  :rule-classes :congruence)