		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Abs-multiplication-expression

Abstract a multiplication-expression.

Signature
(abs-multiplication-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-multiplication-expression

(defun abs-multiplication-expression (tree)
 (declare (xargs :guard (abnf::treep tree)))
 (let ((__function__ 'abs-multiplication-expression))
  (declare (ignorable __function__))
  (b* (((okf treess)
        (check-tree-nonleaf tree "multiplication-expression")))
   (case (len treess)
    (1 (b* (((okf trees)
             (check-tree-list-list-1 treess))
            ((okf tree) (check-tree-list-1 trees))
            ((okf primary)
             (abs-primary-expression tree)))
         primary))
    (3 (b* (((okf (abnf::tree-list-tuple3 sub))
             (check-tree-list-list-3 treess))
            ((okf tree) (check-tree-list-1 sub.1st))
            ((okf sub-mul)
             (abs-multiplication-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-prim)
             (abs-primary-expression tree)))
         (make-expression-mul :arg1 sub-mul
                              :arg2 sub-prim)))
    (otherwise
     (reserrf (list :found-subtree (tree-info-for-error tree))))))))

Theorem: expression-resultp-of-abs-multiplication-expression

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