The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Check fun pat => let '((x, y) : nat * nat) := pat in x + y.

(The previous one is just syntactic sugar for this.)

On Fri, Aug 7, 2020, 17:22 Jim Fehrle <jim.fehrle AT gmail.com> wrote:

Like this?

Check fun '((x, y) : nat * nat) => x + y.

That's helpful, it uses the "pattern ::= pattern10 : term" production.  Can you find one that's a let-in that doesn't get the semantic error?

This doesn't work either:

Definition f x :=
  match x in _ : nat with
    | x => 1
    | _ => 0
  end.

The doc should be specific about where the construct is allowed or not.