Unsolved `case` tactic error position

[leodemoura]

The case tactic is super nice for structuring proofs. However, if it doesn't solve the goal, the error position is very inconvenient. Here is an example:

example (a b : nat) : a + b = b + a :=
begin
   induction b,
   case nat.succ x {  }
--^ the error message is here, it would be much nicer if it was in the } 
end

I'm adding a done tactic before } as a workaround.

example (a b : nat) : a + b = b + a :=
begin
   induction b,
   case nat.succ x {  ...,  done }
                          --^ error message is here if not done.
end

[Kha]

We could add a new special type solve1_itactic which we handle just like { tac } (for which we already special-case the error position); I don't see a nice pure-Lean solution. What do you think?

[leodemoura]

@kha I agree with you. I also didn't see a pure-Lean solution. I like the solve1_itactic. I think it is worth to add it since case is super useful.

[gebner]

We can do something very close in pure Lean using the cur_pos parser: we could use the position after the closing brace as the default position. To get the position inside the braces we'd need something like solve1_itactic.

[Kha]

We can do something very close in pure Lean using the cur_pos parser: we could use the position after the closing brace as the default position.

I tried something like that yesterday, but found the resulting error positions very unconvincing.