michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Add placeholders for transcendental functions in mpbq & mpq

Browse source
This commit is contained in:
Soonho Kong 2013-08-07 12:48:08 -07:00
parent 2670e94398
commit d3dbcadf8b
2 changed files with 46 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
src/util/numerics/mpbq.h
View file

@ -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 */ }
};
}

23
src/util/numerics/mpq.h
View file

@ -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 */ }
};
}