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

Kevin Buzzard (Apr 13 2020 at 07:42):

  obtain h | h : true  true := p,

works

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

oh

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

yeah, just found that out myself

Kenny Lau (Apr 13 2020 at 07:44):

is this a new tactic?

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

somewhat?

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

it's at least 6 months old by now

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

It's just rcases with its arguments in a different order

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

I think the docstring threw me off with obtain ⟨patt⟩ : type := proof

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

which makes it look like the pattern needs to be in brackets

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

it would be nice to add support for type ascriptions inside an rcases pattern so you can also write obtain (h : true) | (h : true) := p,


Last updated: Dec 20 2023 at 11:08 UTC