Skip to Content.
Sympa Menu

coq-club - RE: [Coq-Club] logical simplification

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] logical simplification


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] logical simplification
  • Date: Mon, 14 May 2018 14:13:52 +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 mga06.intel.com
  • Dlp-product: dlpe-windows
  • Dlp-reaction: no-action
  • Dlp-version: 11.0.200.100
  • Ironport-phdr: 9a23:Tk4yCBfNr5YudJ1uVP4k0HlWlGMj4u6mDksu8pMizoh2WeGdxcS/ZB7h7PlgxGXEQZ/co6odzbaO6Oa4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTahb75+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v6bpgRh31hycdLzM38H/ZhNFsjKxVoxyhqR5ww4/Ib46aL/dxZL/RcNcASGZdQspcVSpMCZ68YYsVCOoBOP5Vo4fgqVsJsxS+ChWsBPnoyj9QnnP9wKo00+U9HgHGxgMvAdYOvHrJp9jyMacSUPy6zKnSwjrda/Nawyz96I/WfRAuvfGMR7VwcdLKxEkuEQPFkkufqYj/MzyJ0eQNtnGW4ux9XuyhjG4nrht+ojmpxso0i4nJgJ4VxU7A9Slj3Yk6O9u1Q1N4b968CJZcqi+XOoRsTs8/TWxltzw2xqAItJO6ZiQHxokrywbCZ/GGfYWE+BzuWeiLLTtmin9ofKiziwux/ES80uHwS8i53VJQoiZbktTBuWoB2wLJ5sSZRfZw+kGs0iuV2Q/J8OFLO0U0mLLbK5E/xr4wkYIesUHMHiDshEn7jbWadkQi+ui09evnZq/qqYObN49xkg3+M6IuldKjAekgLwQDUWeW9f6h2LDt8kD1WqhGg/M3n6XDvp3WONwXpqujDA9U1oYj5Qy/DzCj0NkAmHkHLU5KeBKdgIf3P1HCOuv4DfChjFSjjDdr3ffGPqX6D5XMKHjDjKnufbJn50FAzwozyMhT54hIBbEZPPLzRkjxucTEAR8+Kgy42vroCNFg1owFQm+PGa+YMKbKsVCS/O4vIu+MZJUUuDnnMfQl6eTu3jcFngpXdq6wmJATdXqQH/J8Ikzfb2CmyoMKFn5PtQ4jRsTrjkeDWHhdfSDhcbg742RxM4WrApvZQZjpyJmA1yeyE5kcLjRDC1uMGHrsMZ6DVvgQciWKCs5njjEAE7OmTtlyhlmVqAbmxu8/faLv8SoCuMe7jYkn16jojRg3sAdMIYGY2mCJQXtzmzpRFT4wwK1750d6zwXaiPQqs7ljDdVWoshxfEIiL5eFlr57Dcz/XkTKedLbEA/7EOXjOik4S5cK+/FLY0t5HIz93BXM1nL0Rb4Ti7GPQpcz9/CE0g==

Dear Théo,

 

> At least, I try to show them then that there are two possible ways

 

you are absolutely right, I should have mentioned both options, the one restricted to the current state of learning at the given exercise and the long term solution.

 

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


Archive powered by MHonArc 2.6.18.

Top of Page