		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Abs-addition-expression

Abstract a addition-expression.

Signature
(abs-addition-expression tree) → expr-or-err
Arguments: tree — Guard (abnf::treep tree).
Returns: expr-or-err — Type (expression-resultp expr-or-err).

Definitions and Theorems

Function: abs-addition-expression

(defun abs-addition-expression (tree)
 (declare (xargs :guard (abnf::treep tree)))
 (let ((__function__ 'abs-addition-expression))
  (declare (ignorable __function__))
  (b* (((okf treess)
        (check-tree-nonleaf tree "addition-expression")))
   (case (len treess)
    (1 (b* (((okf trees)
             (check-tree-list-list-1 treess))
            ((okf tree) (check-tree-list-1 trees))
            ((okf mult)
             (abs-multiplication-expression tree)))
         mult))
    (3 (b* (((okf (abnf::tree-list-tuple3 sub))
             (check-tree-list-list-3 treess))
            ((okf tree) (check-tree-list-1 sub.1st))
            ((okf sub-add)
             (abs-addition-expression tree))
            ((okf tree) (check-tree-list-1 sub.2nd))
            ((okf &) (check-tree-schars tree "+"))
            ((okf tree) (check-tree-list-1 sub.3rd))
            ((okf sub-mult)
             (abs-multiplication-expression tree)))
         (make-expression-add :arg1 sub-add
                              :arg2 sub-mult)))
    (otherwise
     (reserrf (list :found-subtree (tree-info-for-error tree))))))))

Theorem: expression-resultp-of-abs-addition-expression

(defthm expression-resultp-of-abs-addition-expression
  (b* ((expr-or-err (abs-addition-expression tree)))
    (expression-resultp expr-or-err))
  :rule-classes :rewrite)