Skip to content

Commit 9895e25

Browse files
authored
doc: fix typo in docstring of the cases tactic (#11575)
This PR fixes a typo in the docstring of the `cases` tactic.
1 parent 19e1fe5 commit 9895e25

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/Init/Tactics.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -998,7 +998,7 @@ You can use `with` to provide the variables names for each constructor.
998998
uses tactic `tac₁` for the `nil` case, and `tac₂` for the `cons` case,
999999
and `a` and `as'` are used as names for the new variables introduced.
10001000
- `cases h : e`, where `e` is a variable or an expression,
1001-
performs cases on `e` as above, but also adds a hypothesis `h : e = ...` to each hypothesis,
1001+
performs cases on `e` as above, but also adds a hypothesis `h : e = ...` to each goal,
10021002
where `...` is the constructor instance for that particular case.
10031003
-/
10041004
syntax (name := cases) "cases " elimTarget,+ (" using " term)? (inductionAlts)? : tactic

0 commit comments

Comments
 (0)