Lean4
/-- * `casesm p` applies the `cases` tactic to a hypothesis `h : type`
if `type` matches the pattern `p`.
* `casesm p_1, ..., p_n` applies the `cases` tactic to a hypothesis `h : type`
if `type` matches one of the given patterns.
* `casesm* p` is a more efficient and compact version of `· repeat casesm p`.
It is more efficient because the pattern is compiled once.
* `casesm! p` only applies `cases` if the number of resulting subgoals is <= 1.
Example: The following tactic destructs all conjunctions and disjunctions in the current context.
```
casesm* _ ∨ _, _ ∧ _
```
-/
@[tactic_parser 1000]
public meta def casesM : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.casesM 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "casesm" false✝)
(ParserDescr.unary✝ `optional (ParserDescr.symbol✝ "*")))
(ParserDescr.unary✝ `group (ParserDescr.const✝ `ppSpace)))
((with_annotate_term"sepBy1(" @ParserDescr.sepBy1✝) (ParserDescr.cat✝ `term 0) "," (ParserDescr.symbol✝ ", ")
Bool.false✝))
