		Search-engine friendly clone of the ACL2 documentation.

Concrete-syntax

Grammar-character-listp

Check if all the characters (codes) in a list are valid according to the ABNF grammar.

Signature
(grammar-character-listp x) → std::bool

This lifts grammar-character-p to lists of natural numbers.

Definitions and Theorems

Function: grammar-character-listp

(defun grammar-character-listp (x)
  (declare (xargs :guard (nat-listp x)))
  (let ((__function__ 'grammar-character-listp))
    (declare (ignorable __function__))
    (if (consp x)
        (and (grammar-character-p (car x))
             (grammar-character-listp (cdr x)))
      t)))

Subtopics

Grammar-character-listp-basics: Basic theorems about grammar-character-listp, generated by std::deflist.