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

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

Browse source 
closes #580
This commit is contained in:
Leonardo de Moura 2015-05-05 19:24:51 -07:00
parent a4efefb6ff
commit c7a20644c0
2 changed files with 17 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

@ -1212,7 +1212,7 @@ class rewrite_fn {
level l2 = sort_level(m_unifier_tc->ensure_type(A).first); level l2 = sort_level(m_unifier_tc->ensure_type(A).first);
expr H; expr H;
if (has_dep_elim) { if (has_dep_elim) {
expr Haeqx = mk_app(mk_constant(get_eq_name(), {l1}), A, a, mk_var(0)); expr Haeqx = mk_app(mk_constant(get_eq_name(), {l2}), A, a, 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, a, P, hyp, b, Heq}); H = mk_app({mk_constant(get_eq_rec_name(), {l1, l2}), A, a, P, hyp, b, Heq});
} else { } else {

16
tests/lean/hott/580.hlean Normal file
View file

@ -0,0 +1,16 @@
section
parameters (A : Type) (a b z : A) (add : A → A → A) (le : A → A → Type₀)
local notation 0 := z
local infix + := add
local infix ≤ := le
definition add_zero (x : A) : x + 0 = x := sorry
set_option pp.universes true
definition le_add_of_nonneg_right (H : a + 0 ≤ a + b) : a ≤ a + b :=
begin
rewrite add_zero at H,
exact H
end
end