5
$\begingroup$

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?

$\endgroup$

1 Answer 1

5
$\begingroup$

You can write :

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

See here

$\endgroup$
1
  • $\begingroup$ Thanks. I never would have guessed! $\endgroup$ Apr 3, 2023 at 15:33

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.