Zulip Chat Archive

Stream: general

Topic: obtain bug

Kevin Buzzard (May 28 2022 at 20:09):

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 :=
  obtain ⟨⟨-, h⟩⟩ : nonempty (unique T) := sorry,
  -- no `h` :-(

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

Mario Carneiro (May 28 2022 at 21:07):

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 (May 28 2022 at 21:12):

(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)

Last updated: Aug 03 2023 at 10:10 UTC