dd84829282
This PR modifies the syntax of `induction`, `cases`, and other tactics that use `Lean.Parser.Tactic.inductionAlts`. If a case omits `=> ...` then it is assumed to be `=> ?_`. Example: ```lean example (p : Nat × Nat) : p.1 = p.1 := by cases p with | _ p1 p2 /- case mk p1 p2 : Nat ⊢ (p1, p2).fst = (p1, p2).fst -/ ``` This works with multiple cases as well. Example: ```lean example (n : Nat) : n + 1 = 1 + n := by induction n with | zero | succ n ih /- case zero ⊢ 0 + 1 = 1 + 0 case succ n : Nat ih : n + 1 = 1 + n ⊢ n + 1 + 1 = 1 + (n + 1) -/ ``` The `induction n with | zero | succ n ih` is short for `induction n with | zero | succ n ih => ?_`, which is short for `induction n with | zero => ?_ | succ n ih => ?_`. Note that a consequence of parsing is that only the last alternative can omit `=>`. Any `=>`-free alternatives before an alternative with `=>` will be a part of that alternative. Rationale: - In the future we may require `tacticSeq` to be indented. For one-constructor types, this lets the rest of the tactic sequence not need indentation. - This is a semi-structured alternative to the `cases'`/`induction'` tactics in mathlib. |
||
|---|---|---|
| .. | ||
| bench | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lean-toolchain | ||