Consider the following
Axiom foo : nat -> nat * nat. Definition fooX (x : nat) := let (y, z) := foo x in y + z.
which is fine.
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