max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(frontends/lean/tactic_notation): show error for unsolved focused goals at the end

Browse source 
Fixes #1531.
This commit is contained in:
Gabriel Ebner 2017-04-21 22:53:49 +02:00 • committed by Leonardo de Moura
parent 489b3304bd
commit c2068dae46
3 changed files with 18 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/frontends/lean/tactic_notation.cpp
View file

@ -274,8 +274,8 @@ struct parse_tactic_fn {
auto pos = m_p.pos();
name const & end_tk = m_p.curr_is_token(get_begin_tk()) ? get_end_tk() : get_rcurly_tk();
expr next_tac = parse_block(pos, end_tk);
// auto block_pos = m_p.pos_of(next_tac);
next_tac = mk_tactic_solve1(m_p, next_tac, pos, m_tac_class, m_use_istep && save_info);
auto end_pos = m_p.pos_of(next_tac);
next_tac = mk_tactic_solve1(m_p, next_tac, end_pos, m_tac_class, m_use_istep && save_info);
if (save_info) {
expr info_tac = mk_tactic_save_info(m_p, pos, m_tac_class);
return concat(info_tac, next_tac, pos);

8
tests/lean/auto_quote_error2.lean
View file

@ -37,3 +37,11 @@ begin
exact eq.trans h1 _, -- Error unsolved
end,
end
example (a b : nat) : a = 0 → b = 0 → a = b ∧ b = a :=
begin
intros h1 h2,
split,
{ subst h1 },
--^ error should be at `}`
end

11
tests/lean/auto_quote_error2.lean.expected.out
View file

@ -13,20 +13,20 @@ a_1 : a = b,
a_2 : b = c
⊢ Sort ?
hello world
auto_quote_error2.lean:14:2: error: focus tactic failed, focused goal has not been solved
auto_quote_error2.lean:16:2: error: focus tactic failed, focused goal has not been solved
state:
a b c : ℕ,
a_1 : a = b,
a_2 : b = c
⊢ a = c
hello world
auto_quote_error2.lean:26:2: error: focus tactic failed, focused goal has not been solved
auto_quote_error2.lean:28:2: error: focus tactic failed, focused goal has not been solved
state:
a b c : ℕ,
a_1 : a = b,
a_2 : b = c
⊢ a = ?m_1
auto_quote_error2.lean:37:22: error: don't know how to synthesize placeholder
auto_quote_error2.lean:38:2: error: don't know how to synthesize placeholder
context:
a b c : ℕ,
h1 : a = b,
@ -37,3 +37,8 @@ a b c : ℕ,
h1 : a = b,
h2 : b = c
⊢ a = c
auto_quote_error2.lean:45:14: error: focus tactic failed, focused goal has not been solved
state:
b : ℕ,
h2 : b = 0
⊢ 0 = b