pi-agm
A formal description in Coq of computations of PI using arithmetic-geometric means
Reminder: to generate a makefile, type coq_makefile -f _CoqProject -o Makefile
A formal description in Coq of computations of PI using arithmetic-geometric means
Reminder: to generate a makefile, type coq_makefile -f _CoqProject -o Makefile