Zulip Chat Archive

Stream: new members

Topic: pattern matching exists in tactic mode


Do Nhat Minh (Jun 16 2019 at 16:33):

I have an expression with type \exists x y z, e. Is there any way to quickly get to e? Currently, I have to continually perform cases on the expression, which is quite tiresome.

Reid Barton (Jun 16 2019 at 16:38):

https://github.com/leanprover-community/mathlib/blob/master/docs/tactics.md#rcases

Do Nhat Minh (Jun 16 2019 at 16:50):

Thanks, @Reid Barton!


Last updated: Dec 20 2023 at 11:08 UTC