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

fix(library/simplifier): bug using congr1 theorem

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-02-09 16:24:29 -08:00
parent c45c1748d8
commit 57982135d9
1 changed files with 6 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/library/simplifier/simplifier.cpp
View file

@ -239,8 +239,12 @@ class simplifier_cell::imp {
expr mk_congr1_th(expr const & f_type, expr const & f, expr const & new_f, expr const & a, expr const & Heq_f) {
expr const & A = abst_domain(f_type);
expr B = lower_free_vars(abst_body(f_type), 1, 1);
return ::lean::mk_congr1_th(A, B, f, new_f, Heq_f, a);
if (is_arrow(f_type)) {
expr B = lower_free_vars(abst_body(f_type), 1, 1);
return ::lean::mk_congr1_th(A, B, f, new_f, Heq_f, a);
} else {
return ::lean::mk_hcongr1_th(A, mk_lambda(g_x, A, abst_body(f_type)), f, new_f, Heq_f, a);
}
}
expr mk_congr2_th(expr const & f_type, expr const & a, expr const & new_a, expr const & f, expr Heq_a) {