		Search-engine friendly clone of the ACL2 documentation.

Lispfloat

Er-float-e^x

(Single-precision) floating point e^x.

(er-float-e^x a) is a lispfloat wrapper function.

In the logic this function does not have a definition, but its ACL2::constraints say it returns (mv errmsg ans), where:

errmsg is either a string that indicates an error has occurred (e.g., a rounding error when converting rationals to floats, an overflow, etc.)
ans is a rational.

Definitions and Theorems

Basic Type Theorems

Theorem: er-float-e^x-mvtypes-0

(defthm er-float-e^x-mvtypes-0
  (maybe-stringp (mv-nth 0 (er-float-e^x a)))
  :rule-classes :type-prescription)

Theorem: er-float-e^x-mvtypes-1

(defthm er-float-e^x-mvtypes-1
  (rationalp (mv-nth 1 (er-float-e^x a)))
  :rule-classes :type-prescription)

Rational-Equiv Congruence Rules

Theorem: er-float-e^x-of-rfix-a

(defthm er-float-e^x-of-rfix-a
  (equal (er-float-e^x (rfix a))
         (er-float-e^x a)))

Theorem: er-float-e^x-rational-equiv-congruence-on-a

(defthm er-float-e^x-rational-equiv-congruence-on-a
  (implies (acl2::rational-equiv a a-equiv)
           (equal (er-float-e^x a)
                  (er-float-e^x a-equiv)))
  :rule-classes :congruence)