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

fix(frontends/lean/local_decls): missing '{}' around macro

Browse source
This commit is contained in:
Leonardo de Moura 2015-04-22 12:54:42 -07:00
parent a526cd92ac
commit cdf929d178
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/frontends/lean/local_decls.h
View file

@ -37,11 +37,12 @@ public:
m_entries = cons(mk_pair(k, v), m_entries);
}
void update(name const & k, V const & v) {
if (auto it = m_map.find(k))
if (auto it = m_map.find(k)) {
m_map.insert(k, mk_pair(v, it->second));
else
} else {
lean_unreachable();
}
}
V const * find(name const & k) const { auto it = m_map.find(k); return it ? &(it->first) : nullptr; }
unsigned find_idx(name const & k) const { auto it = m_map.find(k); return it ? it->second : 0; }
bool contains(name const & k) const { return m_map.contains(k); }