cases' — Mathlib

Lean4
/-- The `cases'` tactic is similar to the `cases` tactic in Lean 4 core, but the syntax for giving
names is different:

```
example (h : p ∨ q) : q ∨ p := by
  cases h with
  | inl hp => exact Or.inr hp
  | inr hq => exact Or.inl hq

example (h : p ∨ q) : q ∨ p := by
  cases' h with hp hq
  · exact Or.inr hp
  · exact Or.inl hq

example (h : p ∨ q) : q ∨ p := by
  rcases h with hp | hq
  · exact Or.inr hp
  · exact Or.inl hq
```

Prefer `cases` or `rcases` when possible, because these tactics promote structured proofs.
-/
@[tactic_parser 1000]
public meta def cases' : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `Mathlib.Tactic.cases' 1022
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "cases' " false✝)
          ((with_annotate_term"sepBy1(" @ParserDescr.sepBy1✝) Lean.Parser.Tactic.elimTarget ","
            (ParserDescr.symbol✝ ", ") Bool.false✝))
        (ParserDescr.unary✝ `optional
          (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " using ") (ParserDescr.const✝ `ident))))
      (ParserDescr.unary✝ `optional
        (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " with")
          (ParserDescr.unary✝ `many1
            (ParserDescr.binary✝ `andthen
              (ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ppSpace) (ParserDescr.const✝ `colGt))
              Lean.binderIdent)))))
Похожие утверждения