coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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 11:29:59 +0000
- Accept-language: de-DE, en-US
- Authentication-results: mail2-smtp-roc.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:mSzjMRI8sqtEkrVmUNmcpTZWNBhigK39O0sv0rFitYgXI/3xwZ3uMQTl6Ol3ixeRBMOAtKIC1rKempujcFJDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBWB6kG1uHQZHQy6Pg5oLMz0HJTThoK5zar6r5bUekBDgCe3SbJ0NhS/6wvL4Jo4m4xnf+wKzRbGvmFPY6Ae4GJjJVuem1y0ssKx955q/iAWoPUs+NJaVr3SfqIkQLgeBzMjZTNmrPb3vAXOGFPcrkAXVX8bx0JF
Dear Dominique, Jeff,
yes, sorry for my stupid comments. I knew the usages of Fin as type for index
parameters for functions with a vector parameter (as e.g. standard library
nth), but I didn't see the usefulness of such a type in a function which
actually creates a vector. I guess in
Fixpoint tabulate (n : nat) (A : Set) (f : Fin n -> A) : Vec A n :=
it is known that A is a set with n elements so that f can't be defined for a
different parameter type.
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
- Re: [Coq-Club] Problem with dependent match statement, Terrell, Jeffrey, 09/16/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, Dominique Larchey-Wendling, 09/15/2017
Archive powered by MHonArc 2.6.18.