		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Abs-*-string-literal-element

Abstract a *string-literal-element to a list of Leo characters.

Signature
(abs-*-string-literal-element trees) → chars
Arguments: trees — Guard (abnf::tree-listp trees).
Returns: chars — Type (char-list-resultp chars).

Definitions and Theorems

Function: abs-*-string-literal-element

(defun abs-*-string-literal-element (trees)
  (declare (xargs :guard (abnf::tree-listp trees)))
  (let ((__function__ 'abs-*-string-literal-element))
    (declare (ignorable __function__))
    (b* (((when (endp trees)) nil)
         ((okf char)
          (abs-string-literal-element (car trees)))
         ((okf chars)
          (abs-*-string-literal-element (cdr trees))))
      (cons char chars))))

Theorem: char-list-resultp-of-abs-*-string-literal-element

(defthm char-list-resultp-of-abs-*-string-literal-element
  (b* ((chars (abs-*-string-literal-element trees)))
    (char-list-resultp chars))
  :rule-classes :rewrite)

Theorem: abs-*-string-literal-element-of-tree-list-fix-trees

(defthm abs-*-string-literal-element-of-tree-list-fix-trees
  (equal (abs-*-string-literal-element (abnf::tree-list-fix trees))
         (abs-*-string-literal-element trees)))

Theorem: abs-*-string-literal-element-tree-list-equiv-congruence-on-trees

(defthm
   abs-*-string-literal-element-tree-list-equiv-congruence-on-trees
  (implies (abnf::tree-list-equiv trees trees-equiv)
           (equal (abs-*-string-literal-element trees)
                  (abs-*-string-literal-element trees-equiv)))
  :rule-classes :congruence)