coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Is there a micromega or omega tactic for axiomatic Z?

From: Théo Zimmermann <theo.zimmi AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Is there a micromega or omega tactic for axiomatic Z?
Date: Tue, 22 May 2018 14:14:23 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=theo.zimmi AT gmail.com; spf=Pass smtp.mailfrom=theo.zimmi AT gmail.com; spf=None smtp.helo=postmaster AT mail-ua0-f169.google.com
Ironport-phdr: 9a23:ELJjBh2LuM57CpQPsmDT+DRfVm0co7zxezQtwd8Zse0QLvad9pjvdHbS+e9qxAeQG9mDsLQc06L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHPbQhEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4KdxUBLnhykHODw5/m/ZicJ+kbxVrw66qhNl34LZepuYOOZicq7fe94RWGpPXtxWVyxEGo6ycYsPCPAGPelArIb9pl4OrR6gCgm2AePg0DlIhnnr1qA9z+QhER/J3As6E9MPsXTUqdD1NKYJXOC6yanH1zTDb/dM1Tjh74jIdwksrPeRVrx+dsrRzFMgFwLDjliIpozlODSV1usJs2eF9eZvSeWvi2s/pwFwpDiv2tkjio3Tio0I1F/J8zhyzoUtJdCgVkJ3fdqpHIFTuiyaLYd6XN4uTmNytCony7ALvZi2dzUQxps93R7QcfmHfpCI4h39UOaRJi91hHd/d7K+gxa+6FWgxffgWsWt3lZGsytIn93WunAC0BzT7ceHSv9j8Uu7xTmP0AXT5vlFIUAyi6XbN4YszqAsmpcXq0jOHS/7lF/ogKOLdEgo4PWk5uXjb7n+o5+TLY50igXwMqQ0ncy/BPw1MhQOX2eF/uSwzrzi/Uz8QLVPj/07iabZsJXAKsQaoq61GRNa0oEm6xqnFTepzMwYnWUbLFJCYB+Ik4/pO0jXLP/kCfe/nk+jnSxwx/HGO73hGo/CImLCkLfnZ7Z96lRTxBA9zdBFtNpoDeQKJ+u2UUvsvvTZCAU4Okq62bXJEtJ4g78e2GW4MK6cNa7ItFaO4Kp7P+mBY8kHuTP4KtAq4vfviTkynlpLLvrh5ocedH3tRqcuGE6ee3e52o5QQ1dPhRI3SanRsHPHVDdSY3ioWKdlv2M0DYunCcHIQYX/2eXdjhf+JYVfYyV9Mn7JCW3hLtzWVPIFaSbUKchkwGRdCOqRDrQ53BTrjzfUjrpqKu2OpH8dvJPnkcV8v6jdzE9jszNzCMuZ3ieGSGQmxm4=

Sure! I'll be happy to help.

Le mar. 22 mai 2018 à 14:05, Soegtrop, Michael <michael.soegtrop AT intel.com> a écrit :

Dear Théo,

> All you need is to provide a relation between the two types

perfect, thanks! I admit, I was lacking the imagination that it could work without a computable transfer function. I will give it a try … I hope you are prepared for some more stupid questions ;-)

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] Is there a micromega or omega tactic for axiomatic Z?, Soegtrop, Michael, 05/18/2018
- Re: [Coq-Club] Is there a micromega or omega tactic for axiomatic Z?, Nicolas Magaud, 05/19/2018
  - RE: [Coq-Club] Is there a micromega or omega tactic for axiomatic Z?, Soegtrop, Michael, 05/21/2018
    - Re: [Coq-Club] Is there a micromega or omega tactic for axiomatic Z?, Théo Zimmermann, 05/22/2018
      - RE: [Coq-Club] Is there a micromega or omega tactic for axiomatic Z?, Soegtrop, Michael, 05/22/2018
        
        Re: [Coq-Club] Is there a micromega or omega tactic for axiomatic Z?, Théo Zimmermann, 05/22/2018
        
        RE: [Coq-Club] Is there a micromega or omega tactic for axiomatic Z?, Soegtrop, Michael, 05/25/2018
        
        Re: [Coq-Club] Is there a micromega or omega tactic for axiomatic Z?, Théo Zimmermann, 05/25/2018
        RE: [Coq-Club] Is there a micromega or omega tactic for axiomatic Z?, Soegtrop, Michael, 05/25/2018