From e183ffee08c33eac0e8cf52fba8608a805470b54 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Wed, 10 Dec 2025 08:21:34 +0000 Subject: [PATCH] doc: fix typo in docstring of the `cases` tactic --- src/Init/Tactics.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index 8d14f93813cf..5adbef3abaee 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -998,7 +998,7 @@ You can use `with` to provide the variables names for each constructor. uses tactic `tac₁` for the `nil` case, and `tac₂` for the `cons` case, and `a` and `as'` are used as names for the new variables introduced. - `cases h : e`, where `e` is a variable or an expression, - performs cases on `e` as above, but also adds a hypothesis `h : e = ...` to each hypothesis, + performs cases on `e` as above, but also adds a hypothesis `h : e = ...` to each goal, where `...` is the constructor instance for that particular case. -/ syntax (name := cases) "cases " elimTarget,+ (" using " term)? (inductionAlts)? : tactic