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

fix(library/congr_lemma_manager): issue with reducible annotation when generating congruence lemmas

Browse source
This commit is contained in:
Leonardo de Moura 2015-12-07 12:09:30 -08:00
parent f31553d916
commit 121648dda6
2 changed files with 8 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/congr_lemma_manager.cpp
View file

@ -147,7 +147,7 @@ struct congr_lemma_manager::imp {
optional<result> mk_congr_simp(expr const & fn, buffer<param_info> const & pinfos, buffer<congr_arg_kind> const & kinds) {
try {
expr fn_type = whnf(infer(fn));
expr fn_type = relaxed_whnf(infer(fn));
name e_name("e");
buffer<expr> lhss;
buffer<expr> rhss; // it contains the right-hand-side argument
@ -183,7 +183,7 @@ struct congr_lemma_manager::imp {
eqs.push_back(none_expr());
break;
}}
fn_type = whnf(instantiate(binding_body(fn_type), lhs));
fn_type = relaxed_whnf(instantiate(binding_body(fn_type), lhs));
}
expr lhs = mk_app(fn, lhss);
expr rhs = mk_app(fn, rhss);

6
tests/lean/run/blast_fun_info_bug.lean
View file

@ -1,4 +1,10 @@
definition set (A : Type) := A → Prop
set_option blast.strategy "preprocess"
example {A : Type} (s : set A) (a b : A) : a = b → s a → s b :=
by blast
set_option blast.strategy "cc"
example {A : Type} (s : set A) (a b : A) : a = b → s a → s b :=
by blast