Hi Russell, >I'm not sure that C-CoRN really has a proof of Leibnitz's series for >pi. >The problem is the C-CoRN has two defintions of pi. > >"pi" is defined by Leibnitz's series. >"Pi" is defined by a different sequence. > >However, these two constants are never shown to be equal. "Pi" is used >in >the rest of the development, while "pi" is never touched again (as far >as >I know). > >Proving that Leibnitz's series converges and defining the limit to have >the name "pi" is probably not in the spirit of the task.
I see. Okay, so I'll take Coq away from number 26 then. For now. (And until someone tells me to do otherwise :-)) Freek _______________________________________________ C-CoRN mailing list [email protected] http://mailman.science.ru.nl/mailman/listinfo/c-corn
