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

fix(tests/library/expr_lt): adjust is_lt unit tests to reflect recent modifications

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-20 13:44:44 -08:00
parent 56f5657ee7
commit abfeacb8f0
1 changed files with 0 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/tests/library/expr_lt.cpp
View file

@ -16,7 +16,6 @@ using namespace lean;
static void lt(expr const & e1, expr const & e2, bool expected) { static void lt(expr const & e1, expr const & e2, bool expected) {
lean_assert(is_lt(e1, e2, false) == expected); lean_assert(is_lt(e1, e2, false) == expected);
lean_assert(is_lt(e1, e2, false) == !(e1 == e2 || (is_lt(e2, e1, false)))); lean_assert(is_lt(e1, e2, false) == !(e1 == e2 || (is_lt(e2, e1, false))));
lean_assert(!(e1.hash() < e2.hash()) || (e1 < e2))
} }
static void tst1() { static void tst1() {