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

Fix interval<T>::cosh

Browse source
This commit is contained in:
Soonho Kong 2013-08-14 19:51:54 -07:00
parent cd71218a68
commit 0a2ac88dd1
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/interval/interval_def.h
View file

@ -1314,17 +1314,17 @@ template<typename T> void interval<T>::cosh () {
numeric_traits<T>::set_rounding(false); numeric_traits<T>::set_rounding(false);
numeric_traits<T>::cosh(m_lower); numeric_traits<T>::cosh(m_lower);
numeric_traits<T>::set_rounding(true); numeric_traits<T>::set_rounding(true);
numeric_traits<T>::cosh(m_lower); numeric_traits<T>::cosh(m_upper);
lean_assert(check_invariant()); lean_assert(check_invariant());
return; return;
} }
if(numeric_traits<T>::is_neg(m_upper) || numeric_traits<T>::is_zero(m_upper)) { if(numeric_traits<T>::is_neg(m_upper) || numeric_traits<T>::is_zero(m_upper)) {
// [a, b] where a <= b < 0 // [a, b] where a <= b < 0
numeric_traits<T>::set_rounding(true); std::swap(m_lower, m_upper);
numeric_traits<T>::cosh(m_lower);
numeric_traits<T>::set_rounding(false); numeric_traits<T>::set_rounding(false);
numeric_traits<T>::cosh(m_lower); numeric_traits<T>::cosh(m_lower);
std::swap(m_lower, m_upper); numeric_traits<T>::set_rounding(true);
numeric_traits<T>::cosh(m_upper);
lean_assert(check_invariant()); lean_assert(check_invariant());
return; return;
} }