Abstract a
(abs-*-comma-expression trees) → exprs
Function:
(defun abs-*-comma-expression (trees) (declare (xargs :guard (abnf::tree-listp trees))) (let ((__function__ 'abs-*-comma-expression)) (declare (ignorable __function__)) (b* (((when (endp trees)) nil) ((okf expr) (abs-comma-expression (car trees))) ((okf exprs) (abs-*-comma-expression (cdr trees)))) (cons expr exprs))))
Theorem:
(defthm expression-list-resultp-of-abs-*-comma-expression (b* ((exprs (abs-*-comma-expression trees))) (expression-list-resultp exprs)) :rule-classes :rewrite)
Theorem:
(defthm expression-list-of-abs-*-comma-expression (b* ((?exprs (abs-*-comma-expression trees))) (implies (not (reserrp exprs)) (expression-listp exprs))))
Theorem:
(defthm abs-*-comma-expression-of-tree-list-fix-trees (equal (abs-*-comma-expression (abnf::tree-list-fix trees)) (abs-*-comma-expression trees)))
Theorem:
(defthm abs-*-comma-expression-tree-list-equiv-congruence-on-trees (implies (abnf::tree-list-equiv trees trees-equiv) (equal (abs-*-comma-expression trees) (abs-*-comma-expression trees-equiv))) :rule-classes :congruence)