Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Recursion-and-induction
Boolean-reasoning
Projects
Debugging
Std
Proof-automation
Macro-libraries
ACL2
Theories
Rule-classes
Proof-builder
Hons-and-memoization
Events
History
Parallelism
Programming
Start-here
Real
Debugging
Miscellaneous
Term
Ld
Hints
Type-set
Ordinals
ACL2-customization
With-prover-step-limit
With-prover-time-limit
Set-prover-step-limit
Local-incompatibility
Set-case-split-limitations
Subversive-recursions
Specious-simplification
Defsum
Oracle-timelimit
Thm
Defopener
Gcl
Case-split-limitations
Set-gc-strategy
Default-defun-mode
Top-level
Reader
Ttags-seen
Adviser
Ttree
Abort-soft
Defsums
Gc$
With-timeout
Coi-debug::fail
Expander
Gc-strategy
Coi-debug::assert
Sin-cos
Fast-compute-series
Compute-series
Truncated-integer-sin/cos-table
Truncated-integer-sin/cos-table-fn
Fast-compute-sin
Truncated-integer-sin
Truncated-integer-cos
Fast-compute-cos
Def::doc
Syntax
Subversive-inductions
Output-controls
Macros
Interfacing-tools
Interfacing-tools
Hardware-verification
Software-verification
Testing-utilities
Math
Miscellaneous
Sin-cos
SIN/COS approximations.
Subtopics
Fast-compute-series
Efficient series approximation to SIN/COS.
Compute-series
Series approximation to SIN/COS.
Truncated-integer-sin/cos-table
Create a scaled, truncated integer sin/cos table from
0
to
2*\pi
.
Truncated-integer-sin/cos-table-fn
Helper for
SIN/COS-TABLE-FN
.
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
.
Truncated-integer-sin
Integer approximation to
sin(x) * scale
.
Truncated-integer-cos
Integer approximation to
cos(x) * scale
.
Fast-compute-cos
This function returns the numerator and denominator of a rational approximation to cos(x) (in radians) by itr iterations of
fast-compute-series
.
