We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
cases
1 parent 19e1fe5 commit e183ffeCopy full SHA for e183ffe
src/Init/Tactics.lean
@@ -998,7 +998,7 @@ You can use `with` to provide the variables names for each constructor.
998
uses tactic `tac₁` for the `nil` case, and `tac₂` for the `cons` case,
999
and `a` and `as'` are used as names for the new variables introduced.
1000
- `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,
+ performs cases on `e` as above, but also adds a hypothesis `h : e = ...` to each goal,
1002
where `...` is the constructor instance for that particular case.
1003
-/
1004
syntax (name := cases) "cases " elimTarget,+ (" using " term)? (inductionAlts)? : tactic
0 commit comments