max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/compiler/simp_inductive): check ignore predicate at visit_constant

Browse source
This commit is contained in:
Leonardo de Moura 2016-05-11 16:06:21 -07:00
parent 99716306f1
commit ecc9014d82
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/compiler/simp_inductive.cpp
View file

@ -176,7 +176,7 @@ class simp_inductive_fn : public compiler_step_visitor {
virtual expr visit_constant(expr const & e) override {
name const & n = const_name(e);
if (inductive::is_intro_rule(env(), n)) {
if (inductive::is_intro_rule(env(), n) && !ignore(n)) {
return mk_cnstr(get_constructor_idx(env(), n));
} else {
return e;