		Search-engine friendly clone of the ACL2 documentation.

Check-case

Vl-find-case-equivalent-strings

Find all case-equivalent strings in a string-list.

Signature
(vl-find-case-equivalent-strings x) → equiv-sets
Arguments: x — Guard (string-listp x).
Returns: equiv-sets — Each sub-list is a set of case-equivalent strings that occur within x.
Type (string-list-listp equiv-sets), given the guard.

Definitions and Theorems

Function: vl-find-case-equivalent-strings

(defun vl-find-case-equivalent-strings (x)
  (declare (xargs :guard (string-listp x)))
  (let ((__function__ 'vl-find-case-equivalent-strings))
    (declare (ignorable __function__))
    (b* ((xl (str::downcase-string-list x))
         (dupes (duplicated-members xl))
         (sets (vl-find-case-equivalent-strings-aux dupes x)))
      sets)))

Theorem: string-list-listp-of-vl-find-case-equivalent-strings

(defthm string-list-listp-of-vl-find-case-equivalent-strings
  (implies (and (force (string-listp x)))
           (b* ((equiv-sets (vl-find-case-equivalent-strings x)))
             (string-list-listp equiv-sets)))
  :rule-classes :rewrite)

Subtopics

Vl-find-case-equivalent-strings-aux