more on support of PowerInt and PowerReal

drivers/coq-common.gen

@@ -258,7 +258,7 @@ end
 
 theory real.PowerInt
 
-  prelude "Require Import Rpower."
+  prelude "Require Import Rfunctions."
 
   syntax function power "(powerRZ %1)"
 

examples/check-builtin/intreal.why

+
 theory IntReal
   use import int.Int
   use import real.RealInfix

examples/check-builtin/real.why

@@ -14,3 +14,59 @@ theory TestInfix
   goal Div : 9. /. 2. = 4.5
   goal Inv : inv 5. = 0.2
 end
+
+
+theory SquareTest
+
+  use import real.Square
+
+  lemma Sqrt_zero: sqrt 0.0 = 0.0
+  lemma Sqrt_one: sqrt 1.0 = 1.0
+  lemma Sqrt_four: sqrt 4.0 = 2.0
+
+end
+
+theory ExpLogTest
+
+  use import real.ExpLog
+
+  lemma Log_e : log e = 1.0
+
+end
+
+
+theory PowerIntTest
+
+  use import real.PowerInt
+
+  lemma Pow_2_2 : power 2.0 2 = 4.0
+
+end
+
+
+theory PowerRealTest
+
+  use import real.PowerReal
+
+  lemma Pow_2_2 : pow 2.0 2.0 = 4.0
+
+end
+
+
+theory TrigonometryTest
+
+  use import Real
+  use import Trigonometry
+  use import Square
+
+  lemma Cos_2_pi : cos (2.0 * pi) = 1.0
+  lemma Sin_2_pi : sin (2.0 * pi) = 0.
+  lemma Tan_pi_3 : tan (pi / 2.0) = sqrt 3.0
+  lemma Atan_1   : atan 1.0 = pi / 4.0
+
+end
+
+
+
+
+

theories/real.why

@@ -93,14 +93,6 @@ theory FromInt
 
 end
 
-theory FromIntTest
-
-  use import FromInt
-
-  lemma Test1: from_int 2 = 2.0
-
-end
-
 theory Truncate
 
   use import Real
@@ -178,16 +170,6 @@ theory Square
 
 end
 
-theory SquareTest
-
-  use import Square
-
-  lemma Sqrt_zero: sqrt 0.0 = 0.0
-  lemma Sqrt_one: sqrt 1.0 = 1.0
-  lemma Sqrt_four: sqrt 4.0 = 2.0
-
-end
-
 theory ExpLog
 
   use import Real
@@ -212,15 +194,6 @@ theory ExpLog
 
 end
 
-theory ExpLogTest
-
-  use import ExpLog
-
-  lemma Log_e : log e = 1.0
-
-end
-
-
 theory PowerInt
 
   use int.Int
@@ -232,15 +205,6 @@ theory PowerInt
 
 end
 
-theory PowerIntTest
-
-  use import PowerInt
-
-  lemma Pow_2_2 : power 2.0 2 = 4.0
-
-end
-
-
 theory PowerReal
 
   use import Real
@@ -272,15 +236,6 @@ theory PowerReal
 
 end
 
-theory PowerRealTest
-
-  use import PowerReal
-
-  lemma Pow_2_2 : pow 2.0 2.0 = 4.0
-
-end
-
-
 
 (** Trigonometric functions
     [http://en.wikipedia.org/wiki/Trigonometric_function]
@@ -339,19 +294,6 @@ theory Trigonometry
 
 end
 
-theory TrigonometryTest
-
-  use import Real
-  use import Trigonometry
-  use import Square
-
-  lemma Cos_2_pi : cos (2.0 * pi) = 1.0
-  lemma Sin_2_pi : sin (2.0 * pi) = 0.
-  lemma Tan_pi_3 : tan (pi / 2.0) = sqrt 3.0
-  lemma Atan_1   : atan 1.0 = pi / 4.0
-
-end
-
 (** hyperbolic functions
     [http://en.wikipedia.org/wiki/Hyperbolic_function]
 *)