main.ml 539 Bytes
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1

2
open Why3extract
MARCHE Claude's avatar
MARCHE Claude committed
3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21
open Format

let usage () =
  eprintf "Euler001: sum of all the multiples of 3 or 5 below a given number@.";
  eprintf "Usage: %s <decimal number>@." Sys.argv.(0);
  exit 2

let input =
  if Array.length Sys.argv <> 2 then usage ();
  Sys.argv.(1)

let input_num =
  try
    Why3__BuiltIn.int_constant input
  with _ -> usage ()

let () =
  let a = Euler001__Euler001.solve input_num in
  printf "The sum of all the multiples of 3 or 5 below %s is %s@." 
22
    (Why3__BigInt.to_string input_num) (Why3__BigInt.to_string a)