		Search-engine friendly clone of the ACL2 documentation.

Concrete-syntax

Grammar-character-p

Check if a character (code) is valid according to the ABNF grammar.

Signature
(grammar-character-p char) → yes/no
Arguments: char — Guard (natp char).
Returns: yes/no — Type (booleanp yes/no).

This is based on the definition of character in the ABNF grammar. At some point we should prove that this definition is consistent with that ABNF grammar rule.

Definitions and Theorems

Function: grammar-character-p

(defun grammar-character-p (char)
  (declare (xargs :guard (natp char)))
  (let ((__function__ 'grammar-character-p))
    (declare (ignorable __function__))
    (or (and (<= 9 char) (<= char 13))
        (and (<= 32 char) (<= char 126))
        (and (<= 128 char) (<= char 8233))
        (and (<= 8239 char) (<= char 8293))
        (and (<= 8298 char) (<= char 55295))
        (and (<= 57344 char)
             (<= char 1114111)))))

Theorem: booleanp-of-grammar-character-p

(defthm booleanp-of-grammar-character-p
  (b* ((yes/no (grammar-character-p char)))
    (booleanp yes/no))
  :rule-classes :rewrite)