Integrate the McLaurin series from McLaurinScript into approxPoly
The file mcLaurinSApproxcript.sml has a number of transcendental function series that we do not yet support in approxPoly. We should consider adding them at least there.
This requires defining a function in the style of expPoly_def
for the newly added function and define a function that computes the error bound (see e.g. sinErr_def
). Then one has to show the function equivalent to the summation from the McLaurin theorem (see exp_sum_to_poly
), and then integrate it with the overall soundness proof (approxPoly_soundness
).
File transcLangScript.sml
has the datatype definitions if a transcendental function is not supported in our definitions.