Revision b1e197c030e66d588987087a193fc3a88d8bd5ed authored by Software Heritage on 16 April 2018, 09:06:18 UTC, committed by Software Heritage on 16 April 2018, 09:06:18 UTC
0 parent
computing.v
Require Import BigZ rounding_big.
Eval vm_compute in hpi (10 ^ 1000) 10.
(* Uncomment the next line for the really big computation. Use a version
of coq where native_compute works. *)
(* Time Eval native_compute in million_digit_pi. *)
(* Time Eval vm_compute in (salamin (10 ^ 100) 6 - hpi (10 ^ 100) 6)%bigZ. *)
Computing file changes ...
