		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Binop-for-opcall-name

Accessor function for *binary-opcall-name-to-binop*.

Signature
(binop-for-opcall-name name) → retval
Arguments: name — Guard (stringp name).
Returns: retval — Type (binop-resultp retval).

Definitions and Theorems

Function: binop-for-opcall-name

(defun binop-for-opcall-name (name)
 (declare (xargs :guard (stringp name)))
 (let ((__function__ 'binop-for-opcall-name))
  (declare (ignorable __function__))
  (let
   ((binop? (cdr (assoc-equal name *binary-opcall-name-to-binop*))))
   (if (not (binopp binop?))
       (reserrf (list :unknown-binary-operator-name name))
     binop?))))

Theorem: binop-resultp-of-binop-for-opcall-name

(defthm binop-resultp-of-binop-for-opcall-name
  (b* ((retval (binop-for-opcall-name name)))
    (binop-resultp retval))
  :rule-classes :rewrite)