coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Types in patterns

From: Jason Gross <jasongross9 AT gmail.com>
To: coq-club <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 14:46:54 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-ed1-f45.google.com
Ironport-phdr: 9a23:aYKxxx1mDvNG54QmsmDT+DRfVm0co7zxezQtwd8ZseIWLPad9pjvdHbS+e9qxAeQG9mCtbQU0aGP6fuocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmTuwbalxIRmoogndq9cajIV/Iast1xXFpWdFdf5Lzm1yP1KTmBj85sa0/JF99ilbpuws+c1dX6jkZqo0VbNXAigoPGAz/83rqALMTRCT6XsGU2UZiQRHDg7Y5xznRJjxsy/6tu1g2CmGOMD9UL45VSi+46ptVRTljjoMOTwk/2HNksF/g6xbrxChqRJxwIDafZ+bO+Zlc6zHYd8XX3BMUtpNWyFDBI63cosBD/AGPeZdt4Tzo0EBrQC5BQmqGejhyyVIhnjt3a0hzu8sFgPG0xY7H9IJtnTUo8/1NKAJUeCuyKTF1jrDb/ZM1jf87IjEaAwuofaJXb9pd8fa1EYgGR/fgFqKtYzlIy2a1v4Ls2WD7edtV/6ihm8opgxzozWi2tshhpTJi48Rzl3J9jt0zok3KNO2VUN2YtqpHIVQuSyEN4V7Qt4uTm91tCs71rELtpi2dzUJxpQ/3xPTdeCLfoyS7h/gVOudOyl0iG5mdb6liBu/8U6twfDmWMauylZFtC9Fn8HMtn8T0xzT7dCKSv5n8Ueg3TaDzh7c5fxZLUwtm6rWJJ4szqQ/lpoUtkTDESv2l1vsgKCKcUUk//Ck6+XhYrr4up+RL5F4hh36P6g0mcGyAf40PhYSU2WY4+ix273u8VX8QLpQj/02lqfZsIrdJcQevqO5ARVa0p0k6xa5ADemytMYnWIcLF9BYx+HgI3pNEvPIPD8F/uwn1OskDJzy/DcIrLhGonNLmTEkLr5Ybl97FdcxBMvwtBb+pJbEaoMIOnzW0/0rNzXFAU1Mw2yw+b9CdVyzJkSWWyVAvzRDKSHuliRo+krPuPEMIQSoXP2L+Uvz//ol34w31EHK/qHx5wSPVKxBfNga2qDZmH3yoMDGHwNuAUkS/fx2XWNVDdSYzC5WKdqtWJzM56vEYqWHtPlu7eGxiruRsQHNFADMUiFFDLTT6vBXv4NbCyIJco4y24LULGgT8kq0hT87VammYoiFfLd/2gjjbymzMJ8vrSBmhQ79DgyBMOYgTnUEjNE21gQTjpz55hR5ExwzlDZjPp9iv1cUNFfvrZHDlp8OpnbwOh3Tdv1X1CZcw==

Like this?

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

On Fri, Aug 7, 2020 at 2:10 PM Jim Fehrle <jim.fehrle AT gmail.com> wrote:

@Théo Zimmermann Can you find an example of how a pattern like "x: nat" can be used for let-in? That's the only other construct that uses "pattern". This attempt gives the same error:

psatz (let 'x:nat := 1 in True).

Thanks.

[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