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

fix(library/blast/congruence_closure): fix what look to be typos in congr_key_cmp

Browse source
This commit is contained in:
Ramana Kumar 2016-10-31 10:59:43 +11:00 committed by Leonardo de Moura
parent 97a6fc23aa
commit 82f71e4561
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/blast/congruence_closure.cpp
View file

@ -700,9 +700,9 @@ int congruence_closure::congr_key_cmp::operator()(congr_key const & k1, congr_ke
return quick_cmp(k1.m_R, k2.m_R); return quick_cmp(k1.m_R, k2.m_R);
if (k1.m_eq != k2.m_eq) if (k1.m_eq != k2.m_eq)
return k1.m_eq ? -1 : 1; return k1.m_eq ? -1 : 1;
if (k2.m_iff != k2.m_iff) if (k1.m_iff != k2.m_iff)
return k1.m_iff ? -1 : 1; return k1.m_iff ? -1 : 1;
if (k2.m_symm_rel != k2.m_symm_rel) if (k1.m_symm_rel != k2.m_symm_rel)
return k1.m_symm_rel ? -1 : 1; return k1.m_symm_rel ? -1 : 1;
if (k1.m_eq || k1.m_iff) if (k1.m_eq || k1.m_iff)
return g_cc->cmp_eq_iff_keys(k1, k2); return g_cc->cmp_eq_iff_keys(k1, k2);