		Search-engine friendly clone of the ACL2 documentation.

Floating-point-add-mul

Convert-arith-operation-to-rtl-op

Signature
(convert-arith-operation-to-rtl-op operation) → *
Arguments: operation — Guard (natp operation).

Definitions and Theorems

Function: convert-arith-operation-to-rtl-op$inline

(defun convert-arith-operation-to-rtl-op$inline (operation)
  (declare (xargs :guard (natp operation)))
  (case operation
    (0 'rtl::add)
    (4 'rtl::sub)
    (26 'rtl::mul)
    (28 'rtl::div)
    (otherwise (er hard? 'convert-operation-to-rtl-op
                   "Illegal operation ~x0." operation))))