Library agm.computing
From
Bignums
Require
Import
BigZ
.
Require
Import
rounding_big
.
Eval
vm_compute
in
hpi
(10
^
1000) 10.