		Search-engine friendly clone of the ACL2 documentation.

Sin-cos

Truncated-integer-sin

Integer approximation to sin(x) * scale.

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

Definitions and Theorems

Function: truncated-integer-sin

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