		Search-engine friendly clone of the ACL2 documentation.

Sin-cos

Fast-compute-sin

This function returns the numerator and denominator of a rational approximation to sin(x) (in radians) by itr iterations of fast-compute-series.

Definitions and Theorems

Function: fast-compute-sin

(defun fast-compute-sin (x itr)
  (declare (xargs :guard (and (rationalp x)
                              (integerp itr)
                              (>= itr 0))))
  (fast-compute-series (* (numerator x) (numerator x))
                       (* (denominator x) (denominator x))
                       (numerator x)
                       (numerator x)
                       (denominator x)
                       1 nil itr))