• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
      • 100-theorems
      • Arithmetic
        • Lispfloat
          • Er-double-expt
          • Er-float+
          • Er-float-expt
          • Er-double/
          • Er-double+
          • Er-double*
          • Er-double-
          • Er-float/
          • Er-float*
          • Er-float-
          • Er-float-tan
            • Er-float-sqrt
            • Er-float-sin
            • Er-float-e^x
            • Er-float-cos
            • Er-double-tan
            • Er-double-sqrt
            • Er-double-sin
            • Er-double-e^x
            • Er-double-cos
          • Arithmetic-1
          • Number-theory
          • Proof-by-arith
          • Arith-equivs
          • Include-an-arithmetic-book
          • Number-theory
          • Arithmetic-3
          • Arithmetic-2
          • Arithmetic-light
          • Arithmetic-5
        • Bit-vectors
        • Algebra
      • Testing-utilities
    • Lispfloat

    Er-float-tan

    (Single-precision) floating point tangent.

    (er-float-tan 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-tan-mvtypes-0

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

    Theorem: er-float-tan-mvtypes-1

    (defthm er-float-tan-mvtypes-1
      (rationalp (mv-nth 1 (er-float-tan a)))
      :rule-classes :type-prescription)
    Rational-Equiv Congruence Rules

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

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

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

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