Zulip Chat Archive
Stream: mathlib4
Topic: split syntax
Yury G. Kudryashov (Jan 12 2023 at 22:40):
What is the syntax of the split tactic in Lean 4? E.g., how do I name the new variables?
James Gallicchio (Jan 12 2023 at 23:08):
next is useful there. not sure if there's a better tactic for what you're asking
Last updated: May 02 2025 at 03:31 UTC