coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Types in patterns

From: Giselle Reis <giselle.mnr AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Types in patterns
Date: Thu, 6 Aug 2020 22:53:07 +0300
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=giselle.mnr AT gmail.com; spf=Pass smtp.mailfrom=giselle.mnr AT gmail.com; spf=None smtp.helo=postmaster AT mail-ot1-f49.google.com
Ironport-phdr: 9a23:oWNT0BdE4yIB0ump4e7RMGvXlGMj4u6mDksu8pMizoh2WeGdxcS4bB7h7PlgxGXEQZ/co6odzbaP7eawASdZvcvJmUtBWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6OPn+FJLMgMSrzeCy/IDYbxlViDanbr5+MRS7oR/Su8UKjoduN6k8xxvUqXZUZupawn9lK0iOlBjm/Mew+5Bj8yVUu/0/8sNLTLv3caclQ7FGFToqK2866tHluhnFVguP+2ATUn4KnRpSAgjK9w/1U5HsuSbnrOV92S2aPcrrTbAoXDmp8qlmRAP0hCoBKjU09nzchM5tg6JBuB+uqBxxzYDXbo+IKvRxYrjQfc8GSWdbQspdSzBND4G6YoASD+QBJ+FYr4zlqlUPrBu+HhejBOfryjBWm3T4wbM10+U6EQrb2wEgENMOsG/Ko9XxMKcdT/q5zKzOzTXZdP5W1jL955LJchAlu/2DQbVwcc/IxEQpCgjKgUmep5b/MDOJyuQCrXKb7+x4WO6yiWMqtg58rzqsy8kjioTEiYYYx07L+yh23Ys4O9K2Rk50b9O5H5Zdqz+XOotyT84jQWxkpjg2x7kJtJC1fiUHzoksyRDYa/yCaYeI4xTjWf6QITd+nnJleaiwiwy88Ui6zOD3S8q60E5SoyZbjtXBsmoB2h/T58SdVPdx41ut1SyA2g3X7OxPPFo6mrDBK5E7x749jpoTvlrHHi/xgEj2ibWZdkQg+uSx7OTnfqjqqoaSN4J7jgzyKKsumsu4AeQ3NggBQXKX9vi71L3m5UH5QbNKgeMqkqTBrpzWOcAWqrS6DgJVyIov9QuzAyu83NkXmXQLNFdFdwiGj4jtNVHOOvf4DfKnjlSjkTdr3O7JPrnlAprTNHTDlbHhfaxm5k5TzQo819Ff55ZOBr4dJ/LzX1f9tMbEAR8hLwy03+HnBc1h2YMZQGKDG7OWMKfPsVCT/e8vOOmNZIoNuDnnMfQl5vjujWU4mVAHZ6Wp04EXOziEGaFtJFzcan7xiP8AF30Lt0wwVr/EklqHBBFSfHu2W6903Dw6E8ryAobYS4SpjfqE2j2TEZhfZ2QAAVeJRyS7P76YUusBPXrBavRqlSYJAOD4Ft0RkCq2vQq/8IJJa+rZ/ipC6MDm3dlxourPzFQ8qW0yAMOa3GWACWpzmzFQHmNk7OVEuUV4j2y7/+1gmfUBTI5c4vpIVkExMpuOl7UrWeC3YRrIe5KycHjjR9ynBT8rSddomo0BZk98H5OpiRWRhic=

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

[Coq-Club] Types in patterns, Giselle Reis, 08/06/2020
- Re: [Coq-Club] Types in patterns, Tej Chajed, 08/07/2020
  - Re: [Coq-Club] Types in patterns, Jim Fehrle, 08/07/2020
    - Re: [Coq-Club] Types in patterns, Jim Fehrle, 08/07/2020
      - Re: [Coq-Club] Types in patterns, Jason Gross, 08/07/2020
        
        Re: [Coq-Club] Types in patterns, Jim Fehrle, 08/07/2020
        
        Re: [Coq-Club] Types in patterns, Jason Gross, 08/08/2020
        
        Re: [Coq-Club] Types in patterns, Jim Fehrle, 08/08/2020