• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
      • Std/lists
      • Std/alists
      • Obags
      • Std/util
      • Std/strings
        • Pretty-printing
        • Printtree
        • Base64
        • Charset-p
          • Defcharset
          • Count-leading-charset
          • Str-count-leading-charset-fast
          • Str-count-leading-charset
          • Chars-in-charset-p
          • Code-in-charset-p
          • Char-in-charset-p
          • Strtok!
          • Cases
          • Concatenation
          • Html-encoding
          • Character-kinds
          • Substrings
          • Strtok
          • Equivalences
          • 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
      • Community
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Charset-p

    Char-in-charset-p

    (char-in-charset-p char set) determines if the character char is a member of the character set set.

    Signature
    (char-in-charset-p char set) → *
    Arguments
    set — Guard (charset-p set).

    Definitions and Theorems

    Function: char-in-charset-p$inline

    (defun char-in-charset-p$inline (char set)
      (declare (type character char))
      (declare (xargs :guard (charset-p set)))
      (let ((acl2::__function__ 'char-in-charset-p))
        (declare (ignorable acl2::__function__))
        (mbe :logic (and (characterp char)
                         (logbitp (char-code char) set))
             :exec (logbitp (the (unsigned-byte 8) (char-code char))
                            set))))

    Theorem: char-in-charset-p-when-not-character

    (defthm char-in-charset-p-when-not-character
      (implies (not (characterp char))
               (not (char-in-charset-p char set))))