• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
        • Soft
        • C
        • Bv
        • Imp-language
        • Event-macros
        • Java
          • Atj
          • Aij
          • Language
            • Syntax
              • Grammar
              • Unicode-escapes
              • Unicode-input-char
              • Escape-sequence
              • Identifiers
              • Primitive-types
              • Reference-types
              • Keywords
              • Unicode-characters
              • Integer-literals
              • String-literals
              • Octal-digits
              • Hexadecimal-digits
              • Decimal-digits
              • Binary-digits
              • Character-literals
                • Unicode-charlit-char
                • Char-literal
                  • Char-literal-fix
                  • Char-literal-case
                  • Char-literal-equiv
                  • Char-literalp
                    • Char-literal-escape
                    • Char-literal-char
                    • Char-literal-kind
                  • Unicode-charlit-char-fix
                  • Unicode-charlit-char-p
                • Null-literal
                • Floating-point-literals
                • Boolean-literals
                • Package-names
                • Literals
              • Semantics
          • Bitcoin
          • Ethereum
          • Yul
          • Zcash
          • ACL2-programming-language
          • Prime-fields
          • Json
          • Syntheto
          • File-io-light
          • Cryptography
          • Number-theory
          • Lists-light
          • Axe
          • Builtins
          • Solidity
          • Helpers
          • Htclient
          • Typed-lists-light
          • Arithmetic-light
        • X86isa
        • Axe
        • Execloader
      • Math
      • Testing-utilities
    • Char-literal

    Char-literalp

    Recognizer for char-literal structures.

    Signature
    (char-literalp x) → *

    Definitions and Theorems

    Function: char-literalp

    (defun char-literalp (x)
      (declare (xargs :guard t))
      (let ((__function__ 'char-literalp))
        (declare (ignorable __function__))
        (and (consp x)
             (cond ((or (atom x) (eq (car x) :char))
                    (and (true-listp (cdr x))
                         (eql (len (cdr x)) 1)
                         (b* ((get (std::da-nth 0 (cdr x))))
                           (unicode-charlit-char-p get))))
                   (t (and (eq (car x) :escape)
                           (and (true-listp (cdr x))
                                (eql (len (cdr x)) 1))
                           (b* ((get (std::da-nth 0 (cdr x))))
                             (escape-sequence-p get))))))))

    Theorem: consp-when-char-literalp

    (defthm consp-when-char-literalp
      (implies (char-literalp x) (consp x))
      :rule-classes :compound-recognizer)