max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: add more detail to the split tactic docs (#1988)

Browse source 
Co-authored-by: Mac <tydeu@hatpress.net>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
This commit is contained in:
Jeremy Salwen 2023-01-09 07:12:39 -05:00 • committed by GitHub
parent de0a569781
commit 60f30addc7
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 10 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/Init/Tactics.lean
View file

@ -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