		Search-engine friendly clone of the ACL2 documentation.

Convenience-constructors

<>

Construct a prose value notation element from a character string.

Signature
(<> charstring) → element
Arguments: charstring — Guard (common-lisp::stringp charstring).
Returns: element — Type (elementp element).

The name of this function is inspired by the ABNF notation <...>, where the brackets form the name of this function.

Definitions and Theorems

Function: <>

(defun <> (charstring)
  (declare (xargs :guard (common-lisp::stringp charstring)))
  (element-prose-val (prose-val charstring)))

Theorem: elementp-of-<>

(defthm elementp-of-<>
  (b* ((element (<> charstring)))
    (elementp element))
  :rule-classes :rewrite)

Theorem: <>-of-str-fix-charstring

(defthm <>-of-str-fix-charstring
  (equal (<> (str-fix charstring))
         (<> charstring)))

Theorem: <>-streqv-congruence-on-charstring

(defthm <>-streqv-congruence-on-charstring
  (implies (acl2::streqv charstring charstring-equiv)
           (equal (<> charstring)
                  (<> charstring-equiv)))
  :rule-classes :congruence)