		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-add-typo-candidate

Signature
(vl-add-typo-candidate ss varname typos) → new-typos
Arguments: ss — Scope where this potential typo occurs.
Guard (vl-scopestack-p ss).; varname — Variable that we think may be misspelled.
Guard (stringp varname).; typos — Fast alist to extend.
Guard (vl-typocandidates-p typos).
Returns: new-typos — Type (vl-typocandidates-p new-typos).

Definitions and Theorems

Function: vl-add-typo-candidate

(defun vl-add-typo-candidate (ss varname typos)
  (declare (xargs :guard (and (vl-scopestack-p ss)
                              (stringp varname)
                              (vl-typocandidates-p typos))))
  (let ((__function__ 'vl-add-typo-candidate))
    (declare (ignorable __function__))
    (b* ((ss (vl-scopestack-fix ss))
         (varname (string-fix varname))
         (typos (vl-typocandidates-fix typos))
         (old (cdr (hons-get ss typos))))
      (hons-acons ss (cons varname old)
                  typos))))

Theorem: vl-typocandidates-p-of-vl-add-typo-candidate

(defthm vl-typocandidates-p-of-vl-add-typo-candidate
  (b* ((new-typos (vl-add-typo-candidate ss varname typos)))
    (vl-typocandidates-p new-typos))
  :rule-classes :rewrite)

Theorem: vl-add-typo-candidate-of-vl-scopestack-fix-ss

(defthm vl-add-typo-candidate-of-vl-scopestack-fix-ss
  (equal (vl-add-typo-candidate (vl-scopestack-fix ss)
                                varname typos)
         (vl-add-typo-candidate ss varname typos)))

Theorem: vl-add-typo-candidate-vl-scopestack-equiv-congruence-on-ss

(defthm vl-add-typo-candidate-vl-scopestack-equiv-congruence-on-ss
  (implies (vl-scopestack-equiv ss ss-equiv)
           (equal (vl-add-typo-candidate ss varname typos)
                  (vl-add-typo-candidate ss-equiv varname typos)))
  :rule-classes :congruence)

Theorem: vl-add-typo-candidate-of-str-fix-varname

(defthm vl-add-typo-candidate-of-str-fix-varname
  (equal (vl-add-typo-candidate ss (str-fix varname)
                                typos)
         (vl-add-typo-candidate ss varname typos)))

Theorem: vl-add-typo-candidate-streqv-congruence-on-varname

(defthm vl-add-typo-candidate-streqv-congruence-on-varname
  (implies (streqv varname varname-equiv)
           (equal (vl-add-typo-candidate ss varname typos)
                  (vl-add-typo-candidate ss varname-equiv typos)))
  :rule-classes :congruence)

Theorem: vl-add-typo-candidate-of-vl-typocandidates-fix-typos

(defthm vl-add-typo-candidate-of-vl-typocandidates-fix-typos
  (equal
       (vl-add-typo-candidate ss
                              varname (vl-typocandidates-fix typos))
       (vl-add-typo-candidate ss varname typos)))

Theorem: vl-add-typo-candidate-vl-typocandidates-equiv-congruence-on-typos

(defthm
  vl-add-typo-candidate-vl-typocandidates-equiv-congruence-on-typos
  (implies (vl-typocandidates-equiv typos typos-equiv)
           (equal (vl-add-typo-candidate ss varname typos)
                  (vl-add-typo-candidate ss varname typos-equiv)))
  :rule-classes :congruence)