induction' — Mathlib

Lean4
/-- The `induction'` tactic is similar to the `induction` tactic in Lean 4 core,
but with slightly different syntax (such as, no requirement to name the constructors).

```
open Nat

example (n : ℕ) : 0 < factorial n := by
  induction' n with n ih
  · rw [factorial_zero]
    simp
  · rw [factorial_succ]
    apply mul_pos (succ_pos n) ih

example (n : ℕ) : 0 < factorial n := by
  induction n
  case zero =>
    rw [factorial_zero]
    simp
  case succ n ih =>
    rw [factorial_succ]
    apply mul_pos (succ_pos n) ih
```
-/
@[tactic_parser 1000]
public meta def induction' : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `Mathlib.Tactic.induction' 1022
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen
          (ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "induction' " 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)))))
      (ParserDescr.unary✝ `optional
        (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " generalizing")
          (ParserDescr.unary✝ `many1
            (ParserDescr.binary✝ `andthen
              (ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ppSpace) (ParserDescr.const✝ `colGt))
              (ParserDescr.const✝ `ident))))))
Похожие утверждения