		Search-engine friendly clone of the ACL2 documentation.

Lispfloat

Er-float-

(Single-precision) floating point subtraction.

(er-float- a b) 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--mvtypes-0

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

Theorem: er-float--mvtypes-1

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

Rational-Equiv Congruence Rules

Theorem: er-float--of-rfix-a

(defthm er-float--of-rfix-a
  (equal (er-float- (rfix a) b)
         (er-float- a b)))

Theorem: er-float--rational-equiv-congruence-on-a

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

Theorem: er-float--of-rfix-b

(defthm er-float--of-rfix-b
  (equal (er-float- a (rfix b))
         (er-float- a b)))

Theorem: er-float--rational-equiv-congruence-on-b

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