coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Avoiding the use of JMeq_eq

From: "John Wiegley" <johnw AT newartisans.com>
To: Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Avoiding the use of JMeq_eq
Date: Sat, 27 May 2017 15:27:04 -0700
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jwiegley AT gmail.com; spf=Pass smtp.mailfrom=jwiegley AT gmail.com; spf=None smtp.helo=postmaster AT mail-pg0-f49.google.com
Ironport-phdr: 9a23:0RdC6hy5LlVh6pzXCy+O+j09IxM/srCxBDY+r6Qd2usQIJqq85mqBkHD//Il1AaPBtSFra8bw6qO6ua7CDNGuc7A+Fk5M7VyFDY9yv8q1zQ6B8CEDUCpZNXLVAcdWPp4aVl+4nugOlJUEsutL3fbo3m18CJAUk6nbVk9Kev6AJPdgNqq3O6u5ZLTfx9IhD2gar9uMRm6twvcu80XjId4Kqs8yAbCrn9Ud+hL329lK1aekhTm6sus4JJv9jlbtu48+cJHTaj1cKM0QKBCAjghL247+tDguwPZTQuI6HscU2EWnQRNDgPY8hz0XYr/vzXjuOZl1yaUIcP5TbYvWTS/9KhrUwPniD0GNzEi7m7ajNF7gb9BrxKgoxx/xJPUYJ2QOfFjcK7RYc8WSGxcVctKSSdPHp2zYJcOD+oZPOZXsY/9p0cVrRCjAQWgHf7jxiNUinPz26AxzuYvHhzc3AE4H9wArmnao9f7OqcVUu61wqfHwjrfYP5NxTfx9JLFfgw9rfyWQb59d9fax0k1FwPCi1WdsYLpMTeS1uQNtWiQ8upvVeOxhG4orwF+vDiuyskxgYTOhIIVzVDE9SN3wYsuI923VkB6bsS+EJtMtiGaLJF5QsU5Q21ypCk6zbgGtIe9cSMXxponwBvfZOaGc4iO+h/jUvieIDlii3J/ZLK/hg2y/lKmyu3nTMW7zFFKri9Dn9LRtX4NzwTe58qIR/dn40utxzaC2xrQ5+xKO0w5mq7WJ4Yjz7MxjJYfr0rOEyDslEj3iKKabFgo9+es5unhf77ovIWTN5VuhQH7KqkumtKwAeA/MgUWWmiU4+W81Ln68U3hT7VGkuQ6kqfWvZ3eP8gbqam5Awha0oYn9RmzFSup0NMdnXUfLVJFfgyIj5TxNlzML/30F+qzj0qsnTtxxP3LMKftD5rJI3TblbfuZ7d960pSyAopytBf4opZCrMPIfLyREDxu9jYAQE5MgGvzObnDc9y1oIaWW6VHqCZN6bSvUeS5u0zO+mMeJMVuDHlJvc54P7ulGY1lkMZfam0xpQac2u4H/RjI0WBe3XgmNYBEWEQvgo/VuPmklOCUSQAL0q1Co474zA9CZu7AM/nT5qmgLGQmRi2GJFSZ2ZJQgSAFnLpcYSdRvpKbCuIKc9sg3kbWL6tT44n2jmqsxX7wvxpNLyH1DcfsMep9t914aXslBw98TFlRYzJ0WaNSX5cmG4XTiUq3bt2p1c7wVCGh/sry8dEHMBesqsaGjwxMoTRmqkjU4j/
Organization: New Artisans LLC

>>>>> "DL" == Dominique Larchey-Wendling
>>>>> <dominique.larchey-wendling AT loria.fr>
>>>>> writes:

DL> However, using "proof-style programming" (tactics), the type is much
DL> easier to define/write. See the type definition RoofHom_inv_t and the
DL> generated term.

This will do quite nicely, thank you Dominique!

--
John Wiegley GPG fingerprint = 4710 CF98 AF9B 327B B80F
http://newartisans.com 60E1 46C4 BD1A 7AC1 4BA2

[Coq-Club] Avoiding the use of JMeq_eq, John Wiegley, 05/26/2017
- Re: [Coq-Club] Avoiding the use of JMeq_eq, Dominique Larchey-Wendling, 05/26/2017
  - Re: [Coq-Club] Avoiding the use of JMeq_eq, Dominique Larchey-Wendling, 05/27/2017
    - Re: [Coq-Club] Avoiding the use of JMeq_eq, John Wiegley, 05/28/2017
- Re: [Coq-Club] Avoiding the use of JMeq_eq, Emilio Jesús Gallego Arias, 05/26/2017
  - Re: [Coq-Club] Avoiding the use of JMeq_eq, Emilio Jesús Gallego Arias, 05/26/2017