Abstract an
(abs-annotation tree) → ann
Function:
(defun abs-annotation (tree) (declare (xargs :guard (abnf::treep tree))) (let ((__function__ 'abs-annotation)) (declare (ignorable __function__)) (b* (((okf (abnf::tree-list-tuple2 sub)) (abnf::check-tree-nonleaf-2 tree "annotation")) ((okf tree) (abnf::check-tree-list-1 sub.1st)) ((okf &) (abnf::check-tree-ichars tree "@")) ((okf tree) (abnf::check-tree-list-1 sub.2nd)) ((okf id) (abs-identifier tree))) (make-annotation :name id))))
Theorem:
(defthm annotation-resultp-of-abs-annotation (b* ((ann (abs-annotation tree))) (annotation-resultp ann)) :rule-classes :rewrite)
Theorem:
(defthm abs-annotation-of-tree-fix-tree (equal (abs-annotation (abnf::tree-fix tree)) (abs-annotation tree)))
Theorem:
(defthm abs-annotation-tree-equiv-congruence-on-tree (implies (abnf::tree-equiv tree tree-equiv) (equal (abs-annotation tree) (abs-annotation tree-equiv))) :rule-classes :congruence)