3bab621364
This PR adds the following tactics to the `grind` interactive mode:
- `focus <grind_tac_seq>`
- `next => <grind_tac_seq>`
- `any_goals <grind_tac_seq>`
- `all_goals <grind_tac_seq>`
- `grind_tac <;> grind_tac`
- `cases <anchor>`
- `tactic => <tac_seq>`
Example:
```lean
def g (as : List Nat) :=
match as with
| [] => 1
| [_] => 2
| _::_::_ => 3
example : g bs = 1 → g as ≠ 0 := by
grind [g.eq_def] =>
instantiate
cases #ec88
next => instantiate
next => finish
tactic =>
rw [h_2] at h_1
simp [g] at h_1
```
|
||
|---|---|---|
| .. | ||
| bench | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lake | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lakefile.toml | ||
| lean-toolchain | ||