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

fix(library/tactic/rewrite_tactic): relax reducibility constraints in some parts of the rewrite tactic

Browse source 
fixes #567
This commit is contained in:
Leonardo de Moura 2015-04-30 18:22:58 -07:00
parent d152f38518
commit 0b995c4fe3
2 changed files with 11 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/library/tactic/rewrite_tactic.cpp
View file

@ -1206,8 +1206,8 @@ class rewrite_fn {
expr Pb = instantiate(Px, vidx, b);
expr A = m_tc->infer(a).first;
level l1 = sort_level(m_tc->ensure_type(Pa).first);
level l2 = sort_level(m_tc->ensure_type(A).first);
level l1 = sort_level(m_unifier_tc->ensure_type(Pa).first);
level l2 = sort_level(m_unifier_tc->ensure_type(A).first);
expr H;
if (has_dep_elim) {
expr Haeqx = mk_app(mk_constant(get_eq_name(), {l1}), A, a, mk_var(0));
@ -1257,8 +1257,8 @@ class rewrite_fn {
expr Px = replace_occurrences(Pa, a, occ, vidx);
expr Pb = instantiate(Px, vidx, b);
expr A = m_tc->infer(a).first;
level l1 = sort_level(m_tc->ensure_type(Pa).first);
level l2 = sort_level(m_tc->ensure_type(A).first);
level l1 = sort_level(m_unifier_tc->ensure_type(Pa).first);
level l2 = sort_level(m_unifier_tc->ensure_type(A).first);
expr M = m_g.mk_meta(m_ngen.next(), Pb);
expr H;
if (has_dep_elim) {
@ -1476,7 +1476,7 @@ public:
process_failure(elem, false);
return proof_state_seq();
}
} catch (kernel_exception &) {
} catch (kernel_exception & ex) {
process_failure(elem, true);
return proof_state_seq();
}

6
tests/lean/run/567.lean Normal file
View file

@ -0,0 +1,6 @@
import data.set
example {A : Type} (H : set A) (a x : A) (p : a = x) (l : H x) : H a :=
begin
rewrite p, exact l
end