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: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] Is there a micromega or omega tactic for axiomatic Z?
Date: Tue, 22 May 2018 12:03:44 +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 mga14.intel.com
Dlp-product: dlpe-windows
Dlp-reaction: no-action
Dlp-version: 11.0.200.100
Ironport-phdr: 9a23:zkPG5RYeT8AsZd9DLCwlHUP/LSx+4OfEezUN459isYplN5qZr8i8bnLW6fgltlLVR4KTs6sC17KN9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCazbL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD0fOjA57m/Zl9BwgqxYrhKvpRN/wpLbb46OOfVkYq/QeckXSXZdUstTUSFKH4Oyb5EID+oEJetUoZTzp1wQohuxGQmsHuTvyidQinTr2qM60vguEQHc0wM+G9ICvmnfodLwNKcTTe+1zLPHwivHb/9Mwjf975bHch89ofGWWrJwadHcyUgpFwPZkFqQrZbpMC+S1uQIqmWW6fdrW+yoi24isQ5xoz6vy98tionPmoIa1FTE+T9kz4krI9CzVU11Yca8HZdNsyyWKZF6T8MiTm1yuCs21KcKtYOmcCUK0Jgr2h/SZvKdf4WG7B/vTvidLDl8iX5/Zb6yhAi+/VC9xuD9UsS4ykhGoypKn9XWqHwBzQLf58eDR/Z740yvwyyA1xrJ5eFBOU00lbTUK5omwrMok5oTvl7MEjL5lUnsja+WcFkk9fas6+j9frrmoZqcO5d1igH4LKsuhtSyDfk8PwQQRWSW+eSx2Kfj8EHnWrlGk+A6n6nBvJDfP8sbp6q5AwFP0oYk7hayFzKm0NUEknkHNl1KZhaHg5LyO1HJPv/4Auu/g06rkDdz3P3GP7vhAonTIXjHirvuYbF960tExAop0d9f/45UCq0GIP/rRkDxs8XYAgYlPAyw3uboE85w1pgeWGKKGq+WKrnesV6O5uI1IumDfpUZuDjnK6tt2/m7x3Q+gBoWebSj9ZoRcnGxWPp8aQ3Nan31x9wFDG0ivwwkTeWshkfUAhBJYHPnFZk76z4nEoW+Sc/mR4utibGFlm/vG5xdZmlLDhaXFnrna5+DQ98Nbj6fJolqlTlSBuvpcJMoyRz77Fyy8LFgNOeBonRJ56Km78B84qjorT938DV1C8qH1GTUFjN1mH8FQ3k926Ut+BUhmGfG6rBxhrljLfIW/+lAC15oNJjAwug8ANf3CFqYI4W5DW2+S9DjOgkfC9I8x9hXPBR4FNz70lbC2TanB/kekLnZXJE=

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