Make product argument of lambda function explicit

Stream: new members

[Nicolò Cavalleri]

I do not remember if there is a way of writing λ x : ℕ × ℕ, x.1 + x.2 as something like λ ⟨a, b⟩ : ℕ × ℕ, a + b

[Reid Barton]

You can but (unfortunately) you shouldn't because the latter actually means \lam p, match p with (a, b) -> a + b

[Reid Barton]

which is propositionally equal, but usually a worse definition