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: Fri, 25 May 2018 10:05:33 +0000
Accept-language: de-DE, en-US
Authentication-results: mail3-smtp-sop.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 mga03.intel.com
Ironport-phdr: 9a23:C2RIjBSQd/7ywcI6SFI+XVgjWdpsv+yvbD5Q0YIujvd0So/mwa6yYRSN2/xhgRfzUJnB7Loc0qyK6/umATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfb1/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4qF2QxHqlSgHLSY0/mHJhMJtkKJVrhGvpxJ9zI7VfI6aO+FzcbnBcd4eX2dNQtpdWi5HD4ihb4UPFe0BPeNAooXzulUOqgWxBQawBOP1zT9Inmf61rA93eQgDQ7G3BYvEMwKsHjasd74M6ISUeGpw6nI1zrMcfdW1S3m6IjPbB8hru2MXah3ccrJ0kQvFgXFjkmOpozhJT+ayuMNs22C4udmSOmhhWknqwRrrTiuwMchkojJhoQJyl/a8SV12ps6KsO+RUVmYtCkCINduzyUOoZ5WM8uXm9ltSkgxrEbt5O2fTIGxZUnyhLHdvCKcoaF7gjtWeufOzt0mnxodbalixqv8kWs1vXwWtS13VtOtCZJjNnBu38X2xHd8MSLV/lw80On1D2SzQ7c8PtELloxlafDK54u3Lowlp0LvETGES/5gln6gaGMekUl/Oio9/roYrH8qpCAMI90jxnyMqUomsOhHeQ1KhUCUmaU9OimybHu80L0TK9XgvA4k6TVqpHXKMQDqq68GQBV04Ij6xilDzeh1dQVhXwHLFNZdxKHlYfmJVXOLOrjDfe4nVusnytrx+rBPr35GZjNL37DkKv/crZ58UJT1A0zzdVH65JOFr4BOO7zWlP2tNHAEhA5NBW0z//7B9V5y4MRQnmCArSZMaPXqV+H/PgjI+iKZI8PuTbyMeIp5/D0jSxxpVhIN6KuxN4cbG2yNvVgOUSQJ3T2yJ9VGmAT+wE6UebCiVuYUDcVaWzkDIwm4TRuQrmhAIjfXIe1xPSk3Sy7F5BSLCgSD1GHEX7lc8OfXPoDdDiVOudglCAJUf6qTIp3hkLmjxPz17cydrmcwSYfr5+2jIEktd2Wrgk78HlPN+rY1miMS29umWZRHm032rxypQp2zVLRiPEk0cwdLsRa4rZyail/LYTVlrUoCtbuVwaHddCMGg7/H4eWRAopR9d0+OcgJkZwH9L70ULG0CPyWPkUkaCGANo/9aeOh3U=

Dear Théo,

thanks, then I will continue without requiring Leibnitz equality. Time to learn how to things properly ;-)

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