• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
      • Std/lists
      • Std/alists
      • Obags
      • Std/util
      • Std/strings
        • Pretty-printing
        • Printtree
        • Base64
        • Charset-p
        • Strtok!
        • Cases
        • Concatenation
        • Html-encoding
        • Character-kinds
        • Substrings
        • Strtok
        • Equivalences
          • Charlisteqv
          • Icharlisteqv
          • Istreqv
          • Ichareqv
          • Streqv
          • Chareqv
          • Char-fix
          • Str-fix
        • Url-encoding
        • Lines
        • Explode-implode-equalities
        • Ordering
        • Numbers
        • Pad-trim
        • Coercion
        • Std/strings/digit-to-char
        • Substitution
        • Symbols
      • Std/osets
      • Std/io
      • Std/basic
      • Std/system
      • Std/typed-lists
      • Std/bitsets
      • Std/testing
      • Std/typed-alists
      • Std/stobjs
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Std/strings

Equivalences

Basic equivalence relations.

The string library provides the various ACL2::equivalence relations about characters, character lists, and strings. We end up with the following ACL2::refinement hierarchy:

               equal
   ______________|________________
  |              |                |
chareqv         list-equiv       streqv
  |              |                |
ichareqv        charlisteqv      istreqv
                 |
                icharlisteqv

Subtopics

Charlisteqv
Case-sensitive character-list equivalence test.
Icharlisteqv
Case-insensitive character-list equivalence test.
Istreqv
Case-insensitive string equivalence test.
Ichareqv
Case-insensitive character equivalence test.
Streqv
Case-sensitive string equivalence test.
Chareqv
Case-sensitive character equivalence test.
Char-fix
Coerce to a character.
Str-fix
Coerce to a string.