Zulip Chat Archive

Stream: general

Topic: obtain with |

Mario Carneiro (Apr 13 2020 at 07:30):

I thought that obtain had the same parser as rcases and rintro, but it doesn't work when there is a bar at the top level:

import tactic.basic
example (p : true ∨ true) : true :=
begin
  obtain (h | h) : true ∨ true := p, -- parser fail
  { exact h },
  { exact h },
end

Mario Carneiro (Apr 13 2020 at 07:31):

The parentheses shouldn't even be necessary in this case since the : terminates the pattern, so obtain h | h : true ∨ true := p could even be made to work

Mario Carneiro (Apr 13 2020 at 07:31):

but the docs seem to suggest that a \< \> has to come at the top level

Rob Lewis (Apr 13 2020 at 07:38):

I'm almost certain obtain uses the rcases parser, so this is probably a precedence issue or something. Could you open an issue (if you don't feel like fixing yourself)? I can look into it but not immediately.

Mario Carneiro (Apr 13 2020 at 07:41):

Technically parentheses are not legal there anyway since we are parsing token by token -- they are only supported if there is direct support for them, as in rintro