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

fix(library/tactic/rewrite_tactic): bug in HoTT mode

Browse source
This commit is contained in:
Leonardo de Moura 2015-02-13 10:09:18 -08:00
parent 80e1ac2c4f
commit 98960cbeda
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/tactic/rewrite_tactic.cpp
View file

@ -993,7 +993,7 @@ class rewrite_fn {
expr M = m_g.mk_meta(m_ngen.next(), Pb); expr M = m_g.mk_meta(m_ngen.next(), Pb);
expr H; expr H;
if (has_dep_elim) { if (has_dep_elim) {
expr Haeqx = mk_app(mk_constant(get_eq_name(), {l1}), A, b, mk_var(0)); expr Haeqx = mk_app(mk_constant(get_eq_name(), {l2}), A, b, mk_var(0));
expr P = mk_lambda("x", A, mk_lambda("H", Haeqx, Px)); expr P = mk_lambda("x", A, mk_lambda("H", Haeqx, Px));
H = mk_app({mk_constant(get_eq_rec_name(), {l1, l2}), A, b, P, M, a, Heq}); H = mk_app({mk_constant(get_eq_rec_name(), {l1, l2}), A, b, P, M, a, Heq});
} else { } else {