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

fix(tests/kernel/environment): adjust the test to reflect (recent) change in the normalizer

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-24 21:14:22 -08:00
parent 2aa691ccb3
commit 60ac0b508d
1 changed files with 2 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/tests/kernel/environment.cpp
View file

@ -101,13 +101,8 @@ static void tst3() {
lean_assert(normalize(Const("b"), c_env) == iVal(6)); lean_assert(normalize(Const("b"), c_env) == iVal(6));
c_env->add_definition("c", Int, Const("a")); c_env->add_definition("c", Int, Const("a"));
lean_assert(normalize(Const("c"), c_env) == iVal(3)); lean_assert(normalize(Const("c"), c_env) == iVal(3));
try {
expr r = normalize(Const("c"), env); expr r = normalize(Const("c"), env);
lean_assert(r == iVal(3)); lean_assert(r == Const("c"));
lean_unreachable();
} catch (exception const & ex) {
std::cout << "expected error: " << ex.what() << std::endl;
}
std::cout << "end tst3" << std::endl; std::cout << "end tst3" << std::endl;
} }