		Search-engine friendly clone of the ACL2 documentation.

Literal-evaluation

Eval-string-element

Evaluate a string element to a list of bytes.

Signature
(eval-string-element elem) → bytes
Arguments: elem — Guard (string-elementp elem).
Returns: bytes — Type (ubyte8-listp bytes).

The evaluation of plain string literals involves first turning the string into a sequence of bytes. An escape is turned into a list of bytes as formalized in eval-escape. A single character is turned into a singleton list consisting of the character's code.

Definitions and Theorems

Function: eval-string-element

(defun eval-string-element (elem)
  (declare (xargs :guard (string-elementp elem)))
  (let ((__function__ 'eval-string-element))
    (declare (ignorable __function__))
    (string-element-case elem
                         :char (list (char-code elem.get))
                         :escape (eval-escape elem.get))))

Theorem: ubyte8-listp-of-eval-string-element

(defthm ubyte8-listp-of-eval-string-element
  (b* ((bytes (eval-string-element elem)))
    (ubyte8-listp bytes))
  :rule-classes :rewrite)

Theorem: eval-string-element-of-string-element-fix-elem

(defthm eval-string-element-of-string-element-fix-elem
  (equal (eval-string-element (string-element-fix elem))
         (eval-string-element elem)))

Theorem: eval-string-element-string-element-equiv-congruence-on-elem

(defthm eval-string-element-string-element-equiv-congruence-on-elem
  (implies (string-element-equiv elem elem-equiv)
           (equal (eval-string-element elem)
                  (eval-string-element elem-equiv)))
  :rule-classes :congruence)