obtain bug

Stream: general

[Kevin Buzzard]

I make a habit of tidying up after myself in code when teaching, using the lovely - functionality of rcases to remove everything I know I won't need. But here it seemed to be tidying up too much:

import tactic

lemma obtain_bug {T : Type} : false :=
begin
  obtain ⟨⟨-, h⟩⟩ : nonempty (unique T) := sorry,
  -- no `h` :-(
  sorry,
end

If I replace - with h1 then I get the hypothesis h.

[Mario Carneiro]

I think this is intentional. I mean, if h depends on the deleted argument then they either both have to stay or both have to go, and you have put conflicting recommendations and I guess it goes with the first one. My recommendation is to use _ instead of - here

[Mario Carneiro]

(You could ask why doesn't it report an error, and the reason is that it is hard to report errors in rcases patterns because they can be executed multiple times on different subgoals and if one of them has an error but the other one is conveying useful information it could end up making certain patterns inexpressible. Given this, it is simpler just to have all of them be defined to do something on any input rather than than throwing an error if all subgoals that used the pattern throw the error)