test(tests/kernel/environment): add more tests for environment objects

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-21 12:42:29 -07:00
parent 203a59b682
commit f375ed5f7a

View file

@ -140,10 +140,29 @@ static void tst3() {
lean_assert_eq(checker.whnf(proj1(proj1(mk(id(A, mk(a, b)), b)))), a);
}
class dummy_ext : public environment_extension {};
static void tst4() {
environment env;
try {
env.get_extension(10000);
lean_unreachable();
} catch (kernel_exception & ex) {
std::cout << "expected error: " << ex.what() << "\n";
}
try {
env.update(10000, std::make_shared<dummy_ext>());
lean_unreachable();
} catch (kernel_exception & ex) {
std::cout << "expected error: " << ex.what() << "\n";
}
}
int main() {
save_stack_info();
tst1();
tst2();
tst3();
tst4();
return has_violations() ? 1 : 0;
}