| File | Mode | Size |
|---|---|---|
| AUTHORS | -rw-r--r-- | 18 bytes |
| LICENSE | -rw-r--r-- | 1.0 KB |
| README.md | -rw-r--r-- | 887 bytes |
| _CoqProject | -rw-r--r-- | 175 bytes |
| agmpi.v | -rw-r--r-- | 89.3 KB |
| alg2.v | -rw-r--r-- | 26.3 KB |
| atan_derivative_improper_integral.v | -rw-r--r-- | 4.0 KB |
| computing.v | -rw-r--r-- | 319 bytes |
| elliptic_integral.v | -rw-r--r-- | 36.6 KB |
| filter_Rlt.v | -rw-r--r-- | 22.4 KB |
| generalities.v | -rw-r--r-- | 27.9 KB |
| pi_agm.c | -rw-r--r-- | 1.5 KB |
| rounding2.v | -rw-r--r-- | 44.1 KB |
| rounding_big.v | -rw-r--r-- | 3.7 KB |
| rounding_correct.v | -rw-r--r-- | 113.6 KB |
| test_compare_salamin_hpi.v | -rw-r--r-- | 1.4 KB |
