coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] Problem with dependent match statement

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] Problem with dependent match statement
Date: Fri, 15 Sep 2017 07:10:39 +0000
Accept-language: de-DE, en-US
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga14.intel.com
Dlp-product: dlpe-windows
Dlp-reaction: no-action
Dlp-version: 11.0.0.116
Ironport-phdr: 9a23:UtgPWBASmaJQC1mKhenrUyQJP3N1i/DPJgcQr6AfoPdwSP3ypsbcNUDSrc9gkEXOFd2Crakb26yL6+jJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6i760TlHUB74LE9+Ivn/Mo/UlcW+ke6osdWHaAJRwTG5fLlaLROsrAyXuNNA0qV4LaNkgCDOr3RUYeNOgStNJFmTlhv4rI/k+Z9o8y1dv7Q68MNPTb/9Z4w5S6BVCHItNGVjt56jjgXKUQbavihUaW4RiBcdWwU=

Dear Jeffrey,

your inductive Fin is defined such that you can only construct terms of the
form "Fin (S n)". E.g. there is no way to construct Fin 0, since there is no
constructor of Fin for this term. For this reason there can't be a function
which produces a Fin n from a Fin (S n) for arbitrary n. I guess your
definition of Fin is not what you intended.

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928

[Coq-Club] Problem with dependent match statement, Terrell, Jeffrey, 09/15/2017
- RE: [Coq-Club] Problem with dependent match statement, Soegtrop, Michael, 09/15/2017
- Re: [Coq-Club] Problem with dependent match statement, Jan-Oliver Kaiser, 09/15/2017
  - Re: [Coq-Club] Problem with dependent match statement, Dominique Larchey-Wendling, 09/15/2017
    - Re: [Coq-Club] Problem with dependent match statement, Terrell, Jeffrey, 09/15/2017
    - RE: [Coq-Club] Problem with dependent match statement, Soegtrop, Michael, 09/15/2017
      - Re: [Coq-Club] Problem with dependent match statement, Dominique Larchey-Wendling, 09/15/2017
        
        RE: [Coq-Club] Problem with dependent match statement, Soegtrop, Michael, 09/15/2017
        
        Re: [Coq-Club] Problem with dependent match statement, Terrell, Jeffrey, 09/16/2017
        
        RE: [Coq-Club] Problem with dependent match statement, Soegtrop, Michael, 09/18/2017
        Re: [Coq-Club] Problem with dependent match statement, Terrell, Jeffrey, 09/21/2017
        RE: [Coq-Club] Problem with dependent match statement, Soegtrop, Michael, 09/22/2017