rules for sqrt/pow

scala/info/kwarc/mmt/mitm/rules/Literals.scala

@@ -125,4 +125,5 @@ object IntMinus extends Unary(RealLiterals,Math.intminus,i => 0 - i.asInstanceOf
   StandardDouble =>: StandardDouble
 ) */
 object RealSqrt extends Unary(RealLiterals,Math.sqrt,i => scala.math.sqrt(i.asInstanceOf[Double]))
+object RealPow extends Binary(RealLiterals,Math.realpow,(i,j) => scala.math.pow(i.asInstanceOf[Double],j.asInstanceOf[Double]))
 object RealInv extends Unary(RealLiterals,Math.realinv, i => 1.0 / i.asInstanceOf[Double])
\ No newline at end of file

scala/info/kwarc/mmt/mitm/rules/Symbols.scala

@@ -48,6 +48,7 @@ object Math {
   val realminus = realliterals ? "minus_real_lit"
   val intminus = intliterals ? "minus_int_lit"
   val sqrt = realliterals ? "sqrt"
+  val realpow = realliterals ? "real_pow"
   val realinv = realliterals ? "inv_real_lit"
 
   val string = strings ? "string"

source/math.mmt

@@ -214,13 +214,16 @@ theory RealLiterals : ur:?LF =
 	// square_is_pos : {r : ℝ} ⊦ leq_real_lit 0 (times_real_lit r r) ❙
 	sqrt  : ℝ ⟶ ℝ ❙
 	rule rules?RealSqrt ❙
+
+	real_pow : ℝ ⟶ ℝ ⟶ ℝ ❙
+	rule rules?RealPow ❙
 ❚
      
 theory Literals : ur:?LF =
    include ?RealLiterals ❙
    include ?NatLiterals ❙
    include ?IntLiterals ❙
-   include ?Subtyping ❙
+   //include ?Subtyping ❙
 
    ints_are_real : int_lit <* real_lit ❙