		Search-engine friendly clone of the ACL2 documentation.

Well-formedness

Char-val-wfp

A character value notation is well-formed iff it consists of only non-control ASCII characters, except for the double quote character.

Signature
(char-val-wfp char-val) → yes/no
Arguments: char-val — Guard (char-val-p char-val).
Returns: yes/no — Type (booleanp yes/no).

These allowed characters are consistent with the rule quoted-string in [RFC:4]. That rule allows empty strings, so the rule char-val in [RFC:4] also allows empty strings. An empty character value notation may play the role of the empty sequence of symbols (often denoted by \epsilon in textbooks).

Definitions and Theorems

Function: char-val-wfp

(defun char-val-wfp (char-val)
 (declare (xargs :guard (char-val-p char-val)))
 (b*
  ((allowed-chars (nats=>chars (append (integers-from-to 32 33)
                                       (integers-from-to 35 126)))))
  (char-val-case char-val
                 :sensitive (subsetp (explode char-val.get)
                                     allowed-chars)
                 :insensitive (subsetp (explode char-val.get)
                                       allowed-chars))))

Theorem: booleanp-of-char-val-wfp

(defthm booleanp-of-char-val-wfp
  (b* ((yes/no (char-val-wfp char-val)))
    (booleanp yes/no))
  :rule-classes :rewrite)