rcases

Stream: general

[Reid Barton]

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

[Reid Barton]

import tactic

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

[Reid Barton]

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

[Mario Carneiro]

<_|_>|_

[Mario Carneiro]

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