		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Abs-*-annotation

Abstract a *annotation to a list of annotations.

Signature
(abs-*-annotation trees) → anns
Arguments: trees — Guard (abnf::tree-listp trees).
Returns: anns — Type (annotation-list-resultp anns).

Definitions and Theorems

Function: abs-*-annotation

(defun abs-*-annotation (trees)
  (declare (xargs :guard (abnf::tree-listp trees)))
  (let ((__function__ 'abs-*-annotation))
    (declare (ignorable __function__))
    (b* (((when (endp trees)) nil)
         ((okf ann) (abs-annotation (car trees)))
         ((okf anns)
          (abs-*-annotation (cdr trees))))
      (cons ann anns))))

Theorem: annotation-list-resultp-of-abs-*-annotation

(defthm annotation-list-resultp-of-abs-*-annotation
  (b* ((anns (abs-*-annotation trees)))
    (annotation-list-resultp anns))
  :rule-classes :rewrite)

Theorem: annotation-listp-of-abs-*-annotation

(defthm annotation-listp-of-abs-*-annotation
  (b* ((?anns (abs-*-annotation trees)))
    (implies (not (reserrp anns))
             (annotation-listp anns))))

Theorem: abs-*-annotation-of-tree-list-fix-trees

(defthm abs-*-annotation-of-tree-list-fix-trees
  (equal (abs-*-annotation (abnf::tree-list-fix trees))
         (abs-*-annotation trees)))

Theorem: abs-*-annotation-tree-list-equiv-congruence-on-trees

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