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

chore(library/blast): fix compilation warning

Browse source
This commit is contained in:
Leonardo de Moura 2015-09-21 16:21:21 -07:00
parent bb24421232
commit c0cf54e8d4
1 changed files with 7 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/library/blast/expr.cpp
View file

@ -121,11 +121,18 @@ scope_hash_consing::~scope_hash_consing() {
g_lref_array = reinterpret_cast<expr_array*>(m_lref_array);
}
#ifdef LEAN_DEBUG
static bool is_cached(level const & l) {
lean_assert(g_level_table);
return g_level_table->find(l) != g_level_table->end();
}
static bool is_cached(expr const & l) {
lean_assert(g_expr_table);
return g_expr_table->find(l) != g_expr_table->end();
}
#endif
static level cache(level const & l) {
lean_assert(g_level_table);
auto r = g_level_table->find(l);
@ -135,11 +142,6 @@ static level cache(level const & l) {
return l;
}
static bool is_cached(expr const & l) {
lean_assert(g_expr_table);
return g_expr_table->find(l) != g_expr_table->end();
}
static expr cache(expr const & e) {
lean_assert(g_expr_table);
auto r = g_expr_table->find(e);