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

fix(library/blast/forward/forward_lemma_set): check pattern inference when setting attribute

Browse source
This commit is contained in:
Leonardo de Moura 2015-12-17 22:50:14 -08:00
parent 9a6bd96d6b
commit a7d1625765
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/blast/forward/forward_lemma_set.cpp
View file

@ -8,6 +8,7 @@ Author: Leonardo de Moura
#include "library/scoped_ext.h"
#include "library/attribute_manager.h"
#include "library/blast/forward/forward_lemma_set.h"
#include "library/blast/forward/pattern.h"
namespace lean {
static name * g_name = nullptr;
@ -72,7 +73,8 @@ void initialize_forward_lemma_set() {
forward_lemma_set_ext::initialize();
register_prio_attribute("forward", "forward chaining",
[](environment const & env, io_state const &, name const & d, unsigned prio, name const & ns, bool persistent) {
[](environment const & env, io_state const & ios, name const & d, unsigned prio, name const & ns, bool persistent) {
mk_multipatterns(env, ios, d); // try to create patterns
return add_forward_lemma(env, d, prio, ns, persistent);
},
is_forward_lemma,