		Search-engine friendly clone of the ACL2 documentation.

Unicode-escapes

Abs-unicode-input-character-list

Abstract a list of unicode-input-character trees to a list of Unicode characters.

Signature
(abs-unicode-input-character-list trees) → unicodes
Arguments: trees — Guard (abnf-tree-list-with-root-p trees "unicode-input-character").
Returns: unicodes — Type (unicode-listp unicodes), given the guard.

This lifts abs-unicode-input-character to lists.

Definitions and Theorems

Function: abs-unicode-input-character-list

(defun abs-unicode-input-character-list (trees)
 (declare
  (xargs
      :guard
      (abnf-tree-list-with-root-p trees "unicode-input-character")))
 (let ((__function__ 'abs-unicode-input-character-list))
  (declare (ignorable __function__))
  (cond ((endp trees) nil)
        (t (cons (abs-unicode-input-character (car trees))
                 (abs-unicode-input-character-list (cdr trees)))))))

Theorem: unicode-listp-of-abs-unicode-input-character-list

(defthm unicode-listp-of-abs-unicode-input-character-list
 (implies
  (and
      (abnf-tree-list-with-root-p trees '"unicode-input-character"))
  (b* ((unicodes (abs-unicode-input-character-list trees)))
    (unicode-listp unicodes)))
 :rule-classes :rewrite)

Theorem: len-of-abs-unicode-input-character-list

(defthm len-of-abs-unicode-input-character-list
  (b* ((?unicodes (abs-unicode-input-character-list trees)))
    (equal (len unicodes) (len trees))))