Remove unnecessary TODOs.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
3df6149daa
commit
df054477eb
2 changed files with 42 additions and 42 deletions
|
@ -280,27 +280,27 @@ public:
|
||||||
static void power(mpbq & v, unsigned k) { _power(v, v, k); }
|
static void power(mpbq & v, unsigned k) { _power(v, v, k); }
|
||||||
|
|
||||||
// Transcendental functions
|
// Transcendental functions
|
||||||
static void exp(mpbq & v) { lean_unreachable(); /* TODO */ }
|
static void exp(mpbq & v) { lean_unreachable(); }
|
||||||
static void exp2(mpbq & v) { lean_unreachable(); /* TODO */ }
|
static void exp2(mpbq & v) { lean_unreachable(); }
|
||||||
static void exp10(mpbq & v) { lean_unreachable(); /* TODO */ }
|
static void exp10(mpbq & v) { lean_unreachable(); }
|
||||||
static void log(mpbq & v) { lean_unreachable(); /* TODO */ }
|
static void log(mpbq & v) { lean_unreachable(); }
|
||||||
static void log2(mpbq & v) { lean_unreachable(); /* TODO */ }
|
static void log2(mpbq & v) { lean_unreachable(); }
|
||||||
static void log10(mpbq & v) { lean_unreachable(); /* TODO */ }
|
static void log10(mpbq & v) { lean_unreachable(); }
|
||||||
static void sin(mpbq & v) { lean_unreachable(); /* TODO */ }
|
static void sin(mpbq & v) { lean_unreachable(); }
|
||||||
static void cos(mpbq & v) { lean_unreachable(); /* TODO */ }
|
static void cos(mpbq & v) { lean_unreachable(); }
|
||||||
static void tan(mpbq & v) { lean_unreachable(); /* TODO */ }
|
static void tan(mpbq & v) { lean_unreachable(); }
|
||||||
static void sec(mpbq & v) { lean_unreachable(); /* TODO */ }
|
static void sec(mpbq & v) { lean_unreachable(); }
|
||||||
static void csc(mpbq & v) { lean_unreachable(); /* TODO */ }
|
static void csc(mpbq & v) { lean_unreachable(); }
|
||||||
static void cot(mpbq & v) { lean_unreachable(); /* TODO */ }
|
static void cot(mpbq & v) { lean_unreachable(); }
|
||||||
static void asin(mpbq & v) { lean_unreachable(); /* TODO */ }
|
static void asin(mpbq & v) { lean_unreachable(); }
|
||||||
static void acos(mpbq & v) { lean_unreachable(); /* TODO */ }
|
static void acos(mpbq & v) { lean_unreachable(); }
|
||||||
static void atan(mpbq & v) { lean_unreachable(); /* TODO */ }
|
static void atan(mpbq & v) { lean_unreachable(); }
|
||||||
static void sinh(mpbq & v) { lean_unreachable(); /* TODO */ }
|
static void sinh(mpbq & v) { lean_unreachable(); }
|
||||||
static void cosh(mpbq & v) { lean_unreachable(); /* TODO */ }
|
static void cosh(mpbq & v) { lean_unreachable(); }
|
||||||
static void tanh(mpbq & v) { lean_unreachable(); /* TODO */ }
|
static void tanh(mpbq & v) { lean_unreachable(); }
|
||||||
static void asinh(mpbq & v) { lean_unreachable(); /* TODO */ }
|
static void asinh(mpbq & v) { lean_unreachable(); }
|
||||||
static void acosh(mpbq & v) { lean_unreachable(); /* TODO */ }
|
static void acosh(mpbq & v) { lean_unreachable(); }
|
||||||
static void atanh(mpbq & v) { lean_unreachable(); /* TODO */ }
|
static void atanh(mpbq & v) { lean_unreachable(); }
|
||||||
};
|
};
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|
|
@ -252,27 +252,27 @@ public:
|
||||||
static inline mpq pi_twice_upper() { return pi_u * 2; }
|
static inline mpq pi_twice_upper() { return pi_u * 2; }
|
||||||
|
|
||||||
// Transcendental functions
|
// Transcendental functions
|
||||||
static void exp(mpq & v) { lean_unreachable(); /* TODO */ }
|
static void exp(mpq & v) { lean_unreachable(); }
|
||||||
static void exp2(mpq & v) { lean_unreachable(); /* TODO */ }
|
static void exp2(mpq & v) { lean_unreachable(); }
|
||||||
static void exp10(mpq & v) { lean_unreachable(); /* TODO */ }
|
static void exp10(mpq & v) { lean_unreachable(); }
|
||||||
static void log(mpq & v) { lean_unreachable(); /* TODO */ }
|
static void log(mpq & v) { lean_unreachable(); }
|
||||||
static void log2(mpq & v) { lean_unreachable(); /* TODO */ }
|
static void log2(mpq & v) { lean_unreachable(); }
|
||||||
static void log10(mpq & v) { lean_unreachable(); /* TODO */ }
|
static void log10(mpq & v) { lean_unreachable(); }
|
||||||
static void sin(mpq & v) { lean_unreachable(); /* TODO */ }
|
static void sin(mpq & v) { lean_unreachable(); }
|
||||||
static void cos(mpq & v) { lean_unreachable(); /* TODO */ }
|
static void cos(mpq & v) { lean_unreachable(); }
|
||||||
static void tan(mpq & v) { lean_unreachable(); /* TODO */ }
|
static void tan(mpq & v) { lean_unreachable(); }
|
||||||
static void sec(mpq & v) { lean_unreachable(); /* TODO */ }
|
static void sec(mpq & v) { lean_unreachable(); }
|
||||||
static void csc(mpq & v) { lean_unreachable(); /* TODO */ }
|
static void csc(mpq & v) { lean_unreachable(); }
|
||||||
static void cot(mpq & v) { lean_unreachable(); /* TODO */ }
|
static void cot(mpq & v) { lean_unreachable(); }
|
||||||
static void asin(mpq & v) { lean_unreachable(); /* TODO */ }
|
static void asin(mpq & v) { lean_unreachable(); }
|
||||||
static void acos(mpq & v) { lean_unreachable(); /* TODO */ }
|
static void acos(mpq & v) { lean_unreachable(); }
|
||||||
static void atan(mpq & v) { lean_unreachable(); /* TODO */ }
|
static void atan(mpq & v) { lean_unreachable(); }
|
||||||
static void sinh(mpq & v) { lean_unreachable(); /* TODO */ }
|
static void sinh(mpq & v) { lean_unreachable(); }
|
||||||
static void cosh(mpq & v) { lean_unreachable(); /* TODO */ }
|
static void cosh(mpq & v) { lean_unreachable(); }
|
||||||
static void tanh(mpq & v) { lean_unreachable(); /* TODO */ }
|
static void tanh(mpq & v) { lean_unreachable(); }
|
||||||
static void asinh(mpq & v) { lean_unreachable(); /* TODO */ }
|
static void asinh(mpq & v) { lean_unreachable(); }
|
||||||
static void acosh(mpq & v) { lean_unreachable(); /* TODO */ }
|
static void acosh(mpq & v) { lean_unreachable(); }
|
||||||
static void atanh(mpq & v) { lean_unreachable(); /* TODO */ }
|
static void atanh(mpq & v) { lean_unreachable(); }
|
||||||
};
|
};
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|
Loading…
Reference in a new issue