Commit 2017-08-18 03:14 c5c5b504

feat(tactic/rcases): recursive cases (with patterns) This variant on cases (which I hope will eventually replace cases) allows the specification of patterns for the with clause, composed of anonymous constructors and vertical bars, as in rcases (t : a ∧ b ∨ c ∧ (d ∨ e)) with ⟨ha, hb⟩ | ⟨hc, hd | he⟩. As with destructuring let, if too many arguments are given to a constructor it is treated as a right-associative nested case, i.e. ⟨ha, hb, hc⟩ becomes ⟨ha, ⟨hb, hc⟩⟩ and ha | hb | hc becomes ha | ⟨hb | hc⟩.