From 60f30addc7b3a9c03e3bb12a2f590f07eb6d102c Mon Sep 17 00:00:00 2001 From: Jeremy Salwen Date: Mon, 9 Jan 2023 07:12:39 -0500 Subject: [PATCH] doc: add more detail to the `split` tactic docs (#1988) Co-authored-by: Mac Co-authored-by: Sebastian Ullrich --- src/Init/Tactics.lean | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index 383a0e0409..d8f0164ca0 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -625,8 +625,16 @@ macro_rules | `(tactic| trivial) => `(tactic| simp) syntax "trivial" : tactic /-- -The `split` tactic is useful for breaking nested if-then-else and match expressions in cases. -For a `match` expression with `n` cases, the `split` tactic generates at most `n` subgoals +The `split` tactic is useful for breaking nested if-then-else and `match` expressions into separate cases. +For a `match` expression with `n` cases, the `split` tactic generates at most `n` subgoals. + +For example, given `n : Nat`, and a target `if n = 0 then Q else R`, `split` will generate +one goal with hypothesis `n = 0` and target `Q`, and a second goal with hypothesis +`¬n = 0` and target `R`. Note that the introduced hypothesis is unnamed, and is commonly +renamed used the `case` or `next` tactics. + +- `split` will split the goal (target). +- `split at h` will split the hypothesis `h`. -/ syntax (name := split) "split " (colGt term)? (location)? : tactic