coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] Getting "computing" proof terms with dependent types / reduction of matches with single pattern

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] Getting "computing" proof terms with dependent types / reduction of matches with single pattern
Date: Thu, 8 Sep 2016 15:12:47 +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 mga05.intel.com
Ironport-phdr: 9a23:nyS6tR+4Gp1Dmf9uRHKM819IXTAuvvDOBiVQ1KB92+McTK2v8tzYMVDF4r011RmSDNydtagP27Se8/i5HzdRudDZ6DFKWacPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbvjotuNOU4Y2nL9Oeo0d0Tu612J94E/ushLEu4J0BzHo39FKax95FhDAhatpSv6/dq655V58i5d6LoL/s9EVrjmLexjFeQLRGduD2dgrsbsrFzISRaFznoaSGQf1BRSSUCR5xbjG5z1ryHSt+xn2SDcM9egHp4uXjH3pZxsRRD0kiAfc3Yc8WrXg8F0xuoPpROqpxVyx8jPZ4yaKOB5Zovce88XQSxKWcMHBH8JOZ+1c4ZaV7lJBu1ftYSo/1Y=

Dear Jonathan,

thanks, I think I got it now.

I guess with simple dependent types like vector, it is probably best to use
boolean relational operators as much as possible.

I will see to what this leads ...

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

Re: [Coq-Club] Getting "computing" proof terms with dependent types / reduction of matches with single pattern, (continued)
- Re: [Coq-Club] Getting "computing" proof terms with dependent types / reduction of matches with single pattern, Jason Gross, 09/06/2016