nested patterns in cases?

Stream: lean4

[Jason Gross]

Is there a tactic that allows nested cases such as def x (n : Nat) : Unit := by cases n with | Nat.zero => _ | Nat.succ (Nat.succ _) => _ | Nat.succ _ => _

[Leonardo de Moura]

Lean 4 has a match tactic. The syntax is similar to match expressions

def f : Nat → Nat
  | 0   => 1
  | 1   => 2
  | n+2 => 3

theorem ex (n : Nat) : f n > 0 := by
  match n with
  | 0  => simp [f]
  | 1  => simp [f]
  | Nat.succ (Nat.succ _) => simp [f]

[Jason Gross]

Hm, match, unlike cases, seems to suffer from the same issues in unifying metavariables with expressions as the non-tactic-mode elaborator (point (3) in https://github.com/leanprover/lean4/issues/337)

[Jason Gross]

(I am in fact using cases right now just to get around typing issues with nested patterns in the standard elaborator :-/ . I expect this will be useful in the future, though, so thanks!)