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, Théo Zimmermann <theo.zimmi AT gmail.com>
Subject: Re: [Coq-Club] Types in patterns
Date: Fri, 7 Aug 2020 11:10:20 -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-io1-f42.google.com
Ironport-phdr: 9a23:0M2Odx8YhqIt7P9uRHKM819IXTAuvvDOBiVQ1KB30e0cTK2v8tzYMVDF4r011RmVBNudu6gP0rOJ+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxhJiTanYr5+Mhq6oRjMusQUnIBvNrs/xhzVr3VSZu9Y33loJVWdnxb94se/4ptu+DlOtvwi6sBNT7z0c7w3QrJEAjsmNXs15NDwuhnYUQSP/HocXX4InRdOHgPI8Qv1Xpb1siv9q+p9xCyXNtD4QLwoRTiv6bpgRRn1gykFKjE56nnahcN+jK1ZoByvqR9xzZPKbo6JL/dxZL/RcMkASGZdQspcVSpMCZ68YYsVCOoBOP5VoY38p1sLsBCwBRejBOP1yj9MmHD9wKo30+YgEQHDxgAgEcwBsHTOrNXxKqgfSu+1zKzSwjXCa/Nawyvy6I/Nch04p/yHQL1/f9bLx0Y1CwPFkkufqZbjPz6NyukAsHaW4u5vWO+uj2MqqR19ryahyMooloXEmoYYxkzF+Ch3wYs4O8O1RFJ/bNOgEpZduC+UOpZ5TM4/XWxkpCA3waAFt56jZCUG1ogryhrFZ/GEc4WE+A/vWeeQLDtii39pZrSyjAuo/0e60O3zTMy03U5KriVbltnMsWgA1xnJ5ciGTvtx50ah2TGS2wzK5OFJLl44mbDUK54mxb4wmZ4TvlrZEiDqn0X2ibeadkQi+ue29+TqeqvqqoOYOoNuiQzzMr4iltG+DOk5KAQDUHaX9fy51LL5/E35RLtKjucxkqncqJ3aJ8UbpqujDw9bzIkj6wy/DzO439kDknkHKUhKeBODj4TzJ17OJ/X4Ae+lg1uwiDdr2+zGPrr5D5rRKXjDia7tcqp5605B0wU+1stf5pJRCrEZOv3/QE7xtNrCDh84KQO42ejnCM8unr8ZDGmIG+qSNL7YmV6O/OMmZeeWIMcpuLf6HMok4vvjl3own1lVKbWp0JxRenG9G/VOLECQYH6qidAERzQkpA07Gc7rjRWsXD5JY3v6C6A943c1BYK8CYrrSYWkgbjH1yC+SM4FLltaA0yBRC+7P76PXO0BPXrLc51R1wccXL3kcLcPkBSntQv00b1id7OG9SgRtJal399wtbSKyEMCsAdsBsHY6FmjCmF5mmRSGm0z1aF75E16kxKNjfI+jPtfGtheofhOV1VibMKO/6lBE9n3Hzn5UJKRUl//G4epBDgwSpQ6xNpcO0s=

@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