		Search-engine friendly clone of the ACL2 documentation.

Lispfloat

Er-double-sqrt

(Double-precision) floating point square root.

(er-double-sqrt 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-double-sqrt-mvtypes-0

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

Theorem: er-double-sqrt-mvtypes-1

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

Rational-Equiv Congruence Rules

Theorem: er-double-sqrt-of-rfix-a

(defthm er-double-sqrt-of-rfix-a
  (equal (er-double-sqrt (rfix a))
         (er-double-sqrt a)))

Theorem: er-double-sqrt-rational-equiv-congruence-on-a

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