examples/check-builtin/real.why

   1 theory Test
   2   use real.Real
   3   goal G1 : 5.5 * 10. = 55.
   4   goal G2 : 9. / 3. = 3.
   5   goal G3 : inv 5. = 0.2
   6 end
   7
   8 theory TestInfix
   9   use real.RealInfix
  10   goal Add : 5.5 +. 10. = 15.5
  11   goal Sub : 9. -. 3. = 6.
  12   goal Neg : -. 5. +. 3.5 = -. 1.5
  13   goal Mul : 5.5 *. 10. = 55.
  14   goal Div : 9. /. 2. = 4.5
  15   goal Inv : inv 5. = 0.2
  16 end
  17
  18
  19 theory SquareTest
  20
  21   use real.Square
  22
  23   lemma Sqrt_zero: sqrt 0.0 = 0.0
  24   lemma Sqrt_one: sqrt 1.0 = 1.0
  25   lemma Sqrt_four: sqrt 4.0 = 2.0
  26
  27 end
  28
  29 theory ExpLogTest
  30
  31   use real.ExpLog
  32
  33   lemma Log_e : log e = 1.0
  34
  35 end
  36
  37
  38 theory PowerIntTest
  39
  40   use real.PowerInt
  41
  42   lemma Pow_2_2 : power 2.0 2 = 4.0
  43
  44 end
  45
  46
  47 theory PowerRealTest
  48
  49   use real.PowerReal
  50
  51   lemma Pow_2_2 : pow 2.0 2.0 = 4.0
  52
  53 end
  54
  55
  56 theory TrigonometryTest
  57
  58   use real.Real
  59   use real.Trigonometry
  60   use real.Square
  61
  62   goal Cos_2_pi : cos (2.0 * pi) = 1.0
  63   goal Sin_2_pi : sin (2.0 * pi) = 0.0
  64   goal Tan_pi_4 : tan (pi / 4.0) = 1.0
  65   goal Tan_pi_3 : tan (pi / 3.0) = sqrt 3.0
  66   goal Atan_1   : atan 1.0 = pi / 4.0
  67
  68 end
  69
  70
  71
  72
  73