Why can't I use let bindings to pattern match a 3-tuple in Coq?

Question

Consider the following

Axiom foo : nat -> nat * nat.

Definition fooX (x : nat) := 
  let (y, z) := foo x in
  y + z.

which is fine.

Now, consider

Axiom bar : nat -> nat * nat * nat.

Definition barX1 (x : nat) := 
  match bar x with
  | (y, z, w) => y + z + w
  end.

which is also fine.

But I cannot seem to do this

Definition barX2 (x : nat) :=
  let (y, z, w) := bar x in
  y + z + w.

I get the error Error: Destructing let on this type expects 2 variables.

How do I deconstruct thruples with let pattern matches? Also, does Gallina allow Haskell like where constructs?

Answer 1

You can write :

Definition barX2 (x : nat) :=
  let '(y, z, w) := bar x in
  y + z + w.

See here