The Coq mailing list

[Jim Fehrle <jim.fehrle AT gmail.com>]

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.