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

fix(library/blast/backward/backward_rule_set.cpp): fully annotate the use of map2

Browse source 
Close #904
This commit is contained in:
Soonho Kong 2015-12-01 13:42:25 -05:00
parent 41ff4bc193
commit ff8f24a29b
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/library/blast/backward/backward_rule_set.cpp
View file

@ -15,6 +15,7 @@ namespace lean {
using blast::backward_rule;
using blast::backward_rule_set;
using blast::gexpr;
using std::function;
static name * g_class_name = nullptr;
static std::string * g_key = nullptr;
@ -142,7 +143,7 @@ void backward_rule_set::for_each(std::function<void(head_index const & h, backwa
list<gexpr> backward_rule_set::find(head_index const & h) const {
list<backward_rule> const * rule_list = m_set.find(h);
if (!rule_list) return list<gexpr>();
return map2<gexpr>(*rule_list, [&](backward_rule const & r) { return r.get_proof(); });
return map2<gexpr, backward_rule, function<gexpr(backward_rule)>>(*rule_list, [&](backward_rule const & r) { return r.get_proof(); });
}
void initialize_backward_rule_set() {