formal_lp/old/arith/arith_options.hl

   1 (*************************************)\r
   2 (* Options of the arithmetic library *)\r
   3 (*************************************)\r
   4 module Arith_options = struct\r
   5 \r
   6 (* Base of arithmetic operations with natural numbers *)\r
   7 (* The base should be even in order to represent inv(2) exactly *)\r
   8 let base = 200;;\r
   9 (* If true then special optimized binary operations are used for the natural\r
  10    number arithmetic whenever possible *)\r
  11 let binary = false;;\r
  12 (* If true then operation results are cached for the natural number arithmetic *)\r
  13 let cached = true;;\r
  14 \r
  15 (* Minimal exponent value for floating point numbers \r
  16   (should be even for the square root operation) *)\r
  17 let min_exp = 50;;\r
  18 (* If true, then arithmetic operations with floating point numbers are cached *)\r
  19 let float_cached = true;;\r
  20 \r
  21 end;;\r