Destructuring tuples in function definitions

Stream: lean4

[Ramesh Balaji]

IIUC this documentation is part of lean3: https://leanprover.github.io/reference/declarations.html, but I see you can destructure the cartesian product types (not sure if tuples is the right word) using

def bar₄ (p : ℕ × ℕ) : ℕ :=
let ⟨m, n⟩ := p in m + n

And this let statement works in lean4 as well.

Is there a way to destructure the $\mathbb{N} \times \mathbb{N}$ in the function definition itself? In rust, for example, you can destructure tuples like

fn add((a,b): (u32, u32)) -> u32 {
   a + b
}

Sorry for the dumb question, new to lean :smile:

[Kyle Miller]

Yeah, here's one way you can write it:

def bar₄ : ℕ × ℕ → ℕ :=
  fun ⟨m, n⟩ => m + n

You can also do this:

def bar₄ : ℕ × ℕ → ℕ
  | ⟨m, n⟩ => m + n

[Kyle Miller]

(Usually you'd write (m, n) for products, but it means the same thing.)