coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Types in patterns

From: Jim Fehrle <jim.fehrle AT gmail.com>
To: coq-club AT inria.fr
Cc: Théo Zimmermann <theo.zimmi AT gmail.com>
Subject: Re: [Coq-Club] Types in patterns
Date: Fri, 7 Aug 2020 21:00:56 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jim.fehrle AT gmail.com; spf=Pass smtp.mailfrom=jim.fehrle AT gmail.com; spf=None smtp.helo=postmaster AT mail-il1-f176.google.com
Ironport-phdr: 9a23:oAZ+vBBhfU6YPAa+zH+qUyQJP3N1i/DPJgcQr6AfoPdwSPT5r8bcNUDSrc9gkEXOFd2Cra4d1ayG6Ou/ByQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTagYL5+Nha7oAveusQUgIZpN7o8xAbOrnZUYepd2HlmJUiUnxby58ew+IBs/iFNsP8/9MBOTLv3cb0gQbNXEDopPWY15Nb2tRbYVguA+mEcUmQNnRVWBQXO8Qz3UY3wsiv+sep9xTWaMMjrRr06RTiu86FmQwLuhSwaNTA27XvXh9R/g6JVoh2vpxJxzY3Jbo+LKPVzZbnScc8ASGdbQspdSy5MD4WhZIUPFeoBOuNYopH5qVsPqBu1GAmiC/3vyj9Sgn/5w7Ax3uMjEQHH2QwsBdwOv2rUrNXvMKcdT/u4zKbNzTrZbvNW3S3x55TPchAkuPyBW697fsXNx0c1DQzFkkmQppL/PzOTzukBrWeV4ul8WO+ti2MqqRx8rzqzy8kshYfEm4IYxF/L+Cln3Yo4J9y1RVJ4bNOlDZZdqSGXOoRqT84hTGxkpiY3x7sbspC1eygKzY4oxx/Za/GffIiI4w7jVOaMIThjnn5qZLW/hxO0/EO9yeP8TtG53EhWoidBiNXBtXAA2wbO5sWGS/Zx5Fqt1DSO2g3V9+pKO1o7lbDBJJ4k2rMwloQcsUDEHiLunUX5lq6WdkE99uip7+Trf6zqppGBO4J2iwzyKKsumsu4AeQ3NggBQXKX9vi71L3m5UH5QbNKgeMqkqTBrpzWOcAWqrS6DgJVyIov9heyAja83NgFn3QKLUpJeBedgIjoP1HOLur4DfC6g1m0kjdrxvXGMqfvAprTLnjDirPhcqhm5k5TzQo819Ff55ZOBr4dJ/LzX1f9tMbEAR8hLwy03+HnBc1h2YMZQGKDG7OWMKfPsVCT/e8vOOmNZIoNuDnnMfQl5vjujWU4mVAHZ6Wp04EXOziEGaFtJFzcan7xiP8AF30Lt0wwVr/EklqHBBxSYj6cUqIm4jxzXICnCMHNS4C3hLGp0yKyH5kQbWdDXAPfWUz0fpmJDq9fIBmZJdVsx2RdBOqRDrQ53BTrjzfUjr9uL+7a4Cod7Mux29185umVnhY3p2UtU5atllqVRmQxpVsmAics1fkm80N4w1aHl6N/hq4ATIEB17ZySg4/cKXk4al6BtT1AFyTe96ITBOnRozjD2huEJQ+xNgBZ0s7ENKn3EjO

No, that also gets the error. But I think I learned what I wanted.

Doc update is in https://github.com/coq/coq/pull/12802

On Fri, Aug 7, 2020 at 5:57 PM Jason Gross <jasongross9 AT gmail.com> wrote:

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

[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