		Search-engine friendly clone of the ACL2 documentation.

Sin-cos

Truncated-integer-cos

Integer approximation to cos(x) * scale.

A rational approximation to cos(x), scaled up by scale, and then truncated to an integer.

Definitions and Theorems

Function: truncated-integer-cos

(defun truncated-integer-cos (x itr scale)
  (declare (xargs :guard (and (rationalp x)
                              (integerp itr)
                              (<= 0 itr)
                              (rationalp scale))))
  (mv-let (num denom)
          (fast-compute-cos x itr)
    (truncate (* num scale) denom)))