The Coq mailing list

[Tej Chajed <tchajed AT mit.edu>]

I believe the documentation is incorrect and should not include that syntax. I'm not sure what the semantics would be, either.

Looking at the git history of the documentation, I believe it was automatically extracted from what Coq parses, but it should really be removed since that syntax isn't supported by the match compiler.

Can you file a bug (against the documentation) at https://github.com/coq/coq/issues? Thanks!

On Thu, Aug 6, 2020 at 2:57 PM Giselle Reis <giselle.mnr AT gmail.com> wrote:

Hi all,

According to Coq's documentation
(https://coq.inria.fr/refman/language/core/variants.html#definition-by-cases-match)
it looks like it is possible to have typed patterns in match terms.
However, the following definition (minimal (non)-working example)
fails:

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

The error is "Casts are not supported in this pattern.". (Coq version
8.12, but same happens on 8.11.1)

Am I understanding the documentation wrong, or is there something
missing in the definition?

Thanks!

Giselle