From d3dbcadf8befb7df56999c9b62f1affb56a780b5 Mon Sep 17 00:00:00 2001
From: Soonho Kong <soonhok@cs.cmu.edu>
Date: Wed, 7 Aug 2013 12:48:08 -0700
Subject: [PATCH] Add placeholders for transcendental functions in mpbq & mpq

---
 src/util/numerics/mpbq.h | 23 +++++++++++++++++++++++
 src/util/numerics/mpq.h  | 23 +++++++++++++++++++++++
 2 files changed, 46 insertions(+)

diff --git a/src/util/numerics/mpbq.h b/src/util/numerics/mpbq.h
index afae943d6..7bfa6d8ba 100644
--- a/src/util/numerics/mpbq.h
+++ b/src/util/numerics/mpbq.h
@@ -270,6 +270,29 @@ public:
     static void reset(mpbq & v) { v = 0; }
     // v <- v^k
     static void power(mpbq & v, unsigned k) { _power(v, v, k); }
+
+    // Transcendental functions
+    static void exp(mpq & v)   { lean_unreachable(); /* TODO */ }
+    static void exp2(mpq & v)  { lean_unreachable(); /* TODO */ }
+    static void exp10(mpq & v) { lean_unreachable(); /* TODO */ }
+    static void log(mpq & v)   { lean_unreachable(); /* TODO */ }
+    static void log2(mpq & v)  { lean_unreachable(); /* TODO */ }
+    static void log10(mpq & v) { lean_unreachable(); /* TODO */ }
+    static void sin(mpq & v)   { lean_unreachable(); /* TODO */ }
+    static void cos(mpq & v)   { lean_unreachable(); /* TODO */ }
+    static void tan(mpq & v)   { lean_unreachable(); /* TODO */ }
+    static void sec(mpq & v)   { lean_unreachable(); /* TODO */ }
+    static void csc(mpq & v)   { lean_unreachable(); /* TODO */ }
+    static void cot(mpq & v)   { lean_unreachable(); /* TODO */ }
+    static void asin(mpq & v)  { lean_unreachable(); /* TODO */ }
+    static void acos(mpq & v)  { lean_unreachable(); /* TODO */ }
+    static void atan(mpq & v)  { lean_unreachable(); /* TODO */ }
+    static void sinh(mpq & v)  { lean_unreachable(); /* TODO */ }
+    static void cosh(mpq & v)  { lean_unreachable(); /* TODO */ }
+    static void tanh(mpq & v)  { lean_unreachable(); /* TODO */ }
+    static void asinh(mpq & v) { lean_unreachable(); /* TODO */ }
+    static void acosh(mpq & v) { lean_unreachable(); /* TODO */ }
+    static void atanh(mpq & v) { lean_unreachable(); /* TODO */ }
 };
 
 }
diff --git a/src/util/numerics/mpq.h b/src/util/numerics/mpq.h
index c54edbebd..0b8269079 100644
--- a/src/util/numerics/mpq.h
+++ b/src/util/numerics/mpq.h
@@ -223,6 +223,29 @@ public:
     static void reset(mpq & v) { v = 0; }
     // v <- v^k
     static void power(mpq & v, unsigned k) { _power(v, v, k); }
+
+    // Transcendental functions
+    static void exp(mpq & v)   { lean_unreachable(); /* TODO */ }
+    static void exp2(mpq & v)  { lean_unreachable(); /* TODO */ }
+    static void exp10(mpq & v) { lean_unreachable(); /* TODO */ }
+    static void log(mpq & v)   { lean_unreachable(); /* TODO */ }
+    static void log2(mpq & v)  { lean_unreachable(); /* TODO */ }
+    static void log10(mpq & v) { lean_unreachable(); /* TODO */ }
+    static void sin(mpq & v)   { lean_unreachable(); /* TODO */ }
+    static void cos(mpq & v)   { lean_unreachable(); /* TODO */ }
+    static void tan(mpq & v)   { lean_unreachable(); /* TODO */ }
+    static void sec(mpq & v)   { lean_unreachable(); /* TODO */ }
+    static void csc(mpq & v)   { lean_unreachable(); /* TODO */ }
+    static void cot(mpq & v)   { lean_unreachable(); /* TODO */ }
+    static void asin(mpq & v)  { lean_unreachable(); /* TODO */ }
+    static void acos(mpq & v)  { lean_unreachable(); /* TODO */ }
+    static void atan(mpq & v)  { lean_unreachable(); /* TODO */ }
+    static void sinh(mpq & v)  { lean_unreachable(); /* TODO */ }
+    static void cosh(mpq & v)  { lean_unreachable(); /* TODO */ }
+    static void tanh(mpq & v)  { lean_unreachable(); /* TODO */ }
+    static void asinh(mpq & v) { lean_unreachable(); /* TODO */ }
+    static void acosh(mpq & v) { lean_unreachable(); /* TODO */ }
+    static void atanh(mpq & v) { lean_unreachable(); /* TODO */ }
 };
 
 }