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
Chronological Thread
- 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: Tue, 6 Sep 2016 17:08:40 +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 mga02.intel.com
- Ironport-phdr: 9a23:kdnkPhXj+hqQwV0n6NT5XDBjIq/V8LGtZVwlr6E/grcLSJyIuqrYZhSAt8tkgFKBZ4jH8fUM07OQ6PG5HzFRqs/Y6DhCKMUKDEBVz51O3kQJO42sNw7SFLbSdSs0HcBPBhdO3kqQFgxrIvv4fEDYuXao7DQfSV3VPAtxIfnpSMaJ15zkn7P6x5qGKQ5PnX+2Za54BBSwtwTY8McMy8M2IaEojxDNv3FgeuJMxGouK0jFzDjm4cLltqVk/itMofU5s4ZlUK76dqk8B/QMCTUtM2k44IvwshTMURGI/lMdVHkbllxDBA2Tv0KyZYv4riav7rk14yKdJ8CjFb0=
Dear Jonathan, Jason,
thanks! I will inspect the proof term of this proof and see how I can
incorporate it into the definition of the rev function, so that the rev
function evaluates as expected.
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] Getting "computing" proof terms with dependent types / reduction of matches with single pattern, Soegtrop, Michael, 09/06/2016
- Re: [Coq-Club] Getting "computing" proof terms with dependent types / reduction of matches with single pattern, Matthieu Sozeau, 09/06/2016
- Re: [Coq-Club] Getting "computing" proof terms with dependent types / reduction of matches with single pattern, Jonathan Leivent, 09/06/2016
- Re: [Coq-Club] Getting "computing" proof terms with dependent types / reduction of matches with single pattern, Jonathan Leivent, 09/06/2016
- RE: [Coq-Club] Getting "computing" proof terms with dependent types / reduction of matches with single pattern, Soegtrop, Michael, 09/06/2016
- Re: [Coq-Club] Getting "computing" proof terms with dependent types / reduction of matches with single pattern, Jonathan Leivent, 09/06/2016
- RE: [Coq-Club] Getting "computing" proof terms with dependent types / reduction of matches with single pattern, Soegtrop, Michael, 09/06/2016
- RE: [Coq-Club] Getting "computing" proof terms with dependent types / reduction of matches with single pattern, Soegtrop, Michael, 09/07/2016
- Re: [Coq-Club] Getting "computing" proof terms with dependent types / reduction of matches with single pattern, Guillaume Melquiond, 09/07/2016
- RE: [Coq-Club] Getting "computing" proof terms with dependent types / reduction of matches with single pattern, Soegtrop, Michael, 09/07/2016
- Re: [Coq-Club] Getting "computing" proof terms with dependent types / reduction of matches with single pattern, Guillaume Melquiond, 09/07/2016
- RE: [Coq-Club] Getting "computing" proof terms with dependent types / reduction of matches with single pattern, Soegtrop, Michael, 09/07/2016
- Re: [Coq-Club] Getting "computing" proof terms with dependent types / reduction of matches with single pattern, Guillaume Melquiond, 09/07/2016
- RE: [Coq-Club] Getting "computing" proof terms with dependent types / reduction of matches with single pattern, Soegtrop, Michael, 09/07/2016
- Re: [Coq-Club] Getting "computing" proof terms with dependent types / reduction of matches with single pattern, Guillaume Melquiond, 09/07/2016
- RE: [Coq-Club] Getting "computing" proof terms with dependent types / reduction of matches with single pattern, Soegtrop, Michael, 09/07/2016
- Re: [Coq-Club] Getting "computing" proof terms with dependent types / reduction of matches with single pattern, Jonathan Leivent, 09/07/2016
- Re: [Coq-Club] Getting "computing" proof terms with dependent types / reduction of matches with single pattern, Guillaume Melquiond, 09/07/2016
- RE: [Coq-Club] Getting "computing" proof terms with dependent types / reduction of matches with single pattern, Soegtrop, Michael, 09/07/2016
- Re: [Coq-Club] Getting "computing" proof terms with dependent types / reduction of matches with single pattern, Guillaume Melquiond, 09/07/2016
- Re: [Coq-Club] Getting "computing" proof terms with dependent types / reduction of matches with single pattern, Jonathan Leivent, 09/06/2016
- Re: [Coq-Club] Getting "computing" proof terms with dependent types / reduction of matches with single pattern, Matthieu Sozeau, 09/06/2016
Archive powered by MHonArc 2.6.18.