Abstract a list of
(abs-unicode-input-character-list trees) → unicodes
This lifts abs-unicode-input-character to lists.
Function:
(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:
(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:
(defthm len-of-abs-unicode-input-character-list (b* ((?unicodes (abs-unicode-input-character-list trees))) (equal (len unicodes) (len trees))))