Abstract a
(abs-finalizer tree) → final
Function:
(defun abs-finalizer (tree) (declare (xargs :guard (abnf::treep tree))) (let ((__function__ 'abs-finalizer)) (declare (ignorable __function__)) (b* (((okf (abnf::tree-list-tuple7 sub)) (abnf::check-tree-nonleaf-7 tree "finalizer")) ((okf tree) (abnf::check-tree-list-1 sub.1st)) ((okf &) (abnf::check-tree-schars tree "finalize")) ((okf tree) (abnf::check-tree-list-1 sub.2nd)) ((okf name) (abs-identifier tree)) ((okf tree) (abnf::check-tree-list-1 sub.3rd)) ((okf &) (abnf::check-tree-schars tree "(")) ((okf tree) (abnf::check-tree-list-1 sub.4th)) ((okf params) (abs-?-function-parameters tree)) ((okf tree) (abnf::check-tree-list-1 sub.5th)) ((okf &) (abnf::check-tree-schars tree ")")) ((okf tree) (abnf::check-tree-list-1 sub.6th)) ((okf type?) (abs-?-output-type tree)) ((okf tree) (abnf::check-tree-list-1 sub.7th)) ((okf body) (abs-block tree))) (make-finalizer :name name :inputs params :output type? :body body))))
Theorem:
(defthm finalizer-resultp-of-abs-finalizer (b* ((final (abs-finalizer tree))) (finalizer-resultp final)) :rule-classes :rewrite)
Theorem:
(defthm abs-finalizer-of-tree-fix-tree (equal (abs-finalizer (abnf::tree-fix tree)) (abs-finalizer tree)))
Theorem:
(defthm abs-finalizer-tree-equiv-congruence-on-tree (implies (abnf::tree-equiv tree tree-equiv) (equal (abs-finalizer tree) (abs-finalizer tree-equiv))) :rule-classes :congruence)