		Search-engine friendly clone of the ACL2 documentation.

Well-formedness

Prose-val-wfp

A prose value notation is well-formed iff it consists of only non-control ASCII characters, except for the right angle bracket character.

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

These allowed characters are consistent with the rule prose-val in [RFC:4]. That rule allows empty bracketed strings. Normally prose should be non-empty (so it provides some description), but in the formal semantics any tree matches prose, so the emptiness of prose makes no difference in the formal semantics.

Definitions and Theorems

Function: prose-val-wfp

(defun prose-val-wfp (prose-val)
 (declare (xargs :guard (prose-val-p prose-val)))
 (b*
  ((allowed-chars (nats=>chars (append (integers-from-to 32 61)
                                       (integers-from-to 63 126)))))
  (subsetp (explode (prose-val->get prose-val))
           allowed-chars)))

Theorem: booleanp-of-prose-val-wfp

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