Zulip Chat Archive

Stream: general

Topic: rcases


Reid Barton (Jun 13 2020 at 13:50):

Is it possible to recursively split a sum in the left part of a sum, like rcases x with (_|_)|_?

Reid Barton (Jun 13 2020 at 13:52):

import tactic

example (h : (false  false)  false) : false := begin
  rcases h with (_|_)|_,  -- a zillion errors
end

Reid Barton (Jun 13 2020 at 13:52):

apparently ⟨_|_⟩|_ works here but... perhaps it shouldn't?

Mario Carneiro (Jun 13 2020 at 14:23):

<_|_>|_

Mario Carneiro (Jun 13 2020 at 14:25):

the angle brackets are technically supposed to always show up after an alternation, but they are optional if there is only one element, unless you want to split further


Last updated: Dec 20 2023 at 11:08 UTC