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 10:05:02 +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 mga06.intel.com
- Dlp-product: dlpe-windows
- Dlp-reaction: no-action
- Dlp-version: 11.0.0.116
- Ironport-phdr: 9a23:6KE4BRXqJf2hi92yFw8CZP0QPNvV8LGtZVwlr6E/grcLSJyIuqrYZR2Gt8tkgFKBZ4jH8fUM07OQ6P+wHzFYqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aSV3DMl8/LePsX4XWks6f1uao+pSVbR8CzG62Zqo3JxGrpy3QsNMXiM1sMPBi5AHOpy4CQONbyn9yIkrX1zP97ce58Zopu3BVuvkh/sNEF779cqskV7tAJDUgL20xosbssE+QHkO0+nIAXzBOwVJzCA/f4USiUw==
Dear Jeff,
I wonder what is the advantage of using a definition of Fin n which is
equivalent to False for n=0 in connection with Vectors which exist for n=0.
What bad things would happen if Fin 0 would be defined and equivalent to a
0-tuple of unit rather than something which doesn't exist at all? Is the fact
that Fin 0 -> False used for ex falso quod libet proofs in some places? Since
the 0 length constructor of vectors is trivial I don't see many applications
for this. So unless you really need ex falso quod libet proofs using Fin 0
somewhere, I have doubts that this is the most efficient (in terms of human
time to get things done) way of setting up things.
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.