		Search-engine friendly clone of the ACL2 documentation.

Example-lexer

Idtail-char-p

Recogize characters that are okay in the "tails" of identifiers: letters, numbers, and underscores.

Definitions and Theorems

Function: idtail-char-p

(defun idtail-char-p (x)
  (declare (xargs :guard t))
  (and (characterp x)
       (or (letter-char-p x)
           (number-char-p x)
           (eql x #\_))))

Theorem: booleanp-of-idtail-char-p

(defthm booleanp-of-idtail-char-p
  (booleanp (idtail-char-p x))
  :rule-classes :type-prescription)

Theorem: characterp-when-idtail-char-p

(defthm characterp-when-idtail-char-p
  (implies (idtail-char-p x)
           (characterp x))
  :rule-classes :compound-recognizer)

Subtopics

Idtail-charlist-p: (idtail-charlist-p x) recognizes lists where every element satisfies idtail-char-p.
Idtail-chars: A character set for idtail-char-p.