Append together all the text for a list of tokens.
This is an ordinary defmapappend.
Function:
(defun vl-tokenlist->etext (x) (declare (xargs :guard (vl-tokenlist-p x))) (mbe :logic (if (consp x) (append (vl-token->etext (car x)) (vl-tokenlist->etext (cdr x))) nil) :exec (reverse (vl-tokenlist->etext-exec x nil))))
Function:
(defun vl-tokenlist->etext-exec (x acc) (declare (xargs :guard (vl-tokenlist-p x))) (if (consp x) (vl-tokenlist->etext-exec (cdr x) (revappend (vl-token->etext (car x)) acc)) acc))
Function:
(defun vl-tokenlist->etext (x) (declare (xargs :guard (vl-tokenlist-p x))) (mbe :logic (if (consp x) (append (vl-token->etext (car x)) (vl-tokenlist->etext (cdr x))) nil) :exec (reverse (vl-tokenlist->etext-exec x nil))))
Theorem:
(defthm vl-tokenlist->etext-exec-removal (equal (vl-tokenlist->etext-exec acl2::x acl2::acc) (revappend (vl-tokenlist->etext acl2::x) acl2::acc)) :rule-classes ((:rewrite)))
Theorem:
(defthm set-equiv-congruence-over-vl-tokenlist->etext (implies (set-equiv acl2::x acl2::y) (set-equiv (vl-tokenlist->etext acl2::x) (vl-tokenlist->etext acl2::y))) :rule-classes ((:congruence)))
Theorem:
(defthm subsetp-of-vl-tokenlist->etext-when-subsetp (implies (subsetp acl2::x acl2::y) (subsetp (vl-tokenlist->etext acl2::x) (vl-tokenlist->etext acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm member-in-vl-tokenlist->etext (implies (and (member acl2::k (vl-token->etext acl2::j)) (member acl2::j acl2::x)) (member acl2::k (vl-tokenlist->etext acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm vl-tokenlist->etext-of-list-fix (equal (vl-tokenlist->etext (list-fix acl2::x)) (vl-tokenlist->etext acl2::x)) :rule-classes ((:rewrite)))
Theorem:
(defthm vl-tokenlist->etext-of-append (equal (vl-tokenlist->etext (append acl2::a acl2::b)) (append (vl-tokenlist->etext acl2::a) (vl-tokenlist->etext acl2::b))) :rule-classes ((:rewrite)))
Theorem:
(defthm vl-tokenlist->etext-when-not-consp (implies (not (consp acl2::x)) (equal (vl-tokenlist->etext acl2::x) nil)) :rule-classes ((:rewrite)))
Theorem:
(defthm vl-tokenlist->etext-of-cons (equal (vl-tokenlist->etext (cons acl2::a acl2::b)) (append (vl-token->etext acl2::a) (vl-tokenlist->etext acl2::b))) :rule-classes ((:rewrite)))
Theorem:
(defthm vl-echarlist-p-of-vl-tokenlist->etext (implies (force (vl-tokenlist-p x)) (vl-echarlist-p (vl-tokenlist->etext x))))