		Search-engine friendly clone of the ACL2 documentation.

Character-kinds

Letter/digit/uscore/dollar-char-p

Recognize ASCII letters, decimal digits, underscores, and dollar signs.

Definitions and Theorems

Function: letter/digit/uscore/dollar-char-p

(defun letter/digit/uscore/dollar-char-p (x)
  (declare (xargs :guard t))
  (and (characterp x)
       (b* ((code (char-code x)))
         (or (and (<= (char-code #\A) code)
                  (<= code (char-code #\Z)))
             (and (<= (char-code #\a) code)
                  (<= code (char-code #\z)))
             (and (<= (char-code #\0) code)
                  (<= code (char-code #\9)))
             (eql x #\_)
             (eql x #\$)))))

Theorem: booleanp-of-letter/digit/uscore/dollar-char-p

(defthm booleanp-of-letter/digit/uscore/dollar-char-p
  (booleanp (letter/digit/uscore/dollar-char-p x))
  :rule-classes :type-prescription)

Theorem: characterp-when-letter/digit/uscore/dollar-char-p

(defthm characterp-when-letter/digit/uscore/dollar-char-p
  (implies (letter/digit/uscore/dollar-char-p x)
           (characterp x))
  :rule-classes :compound-recognizer)

Subtopics

Letter/digit/uscore/dollar-charlist-p: (letter/digit/uscore/dollar-charlist-p x) recognizes lists where every element satisfies letter/digit/uscore/dollar-char-p.
Letter/digit/uscore/dollar-chars: A character set for letter/digit/uscore/dollar-char-p.