coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Getting lra to work with canonical rationals

From: Raphaël Cauderlier <raphael.cauderlier AT nomadic-labs.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Getting lra to work with canonical rationals
Date: Fri, 09 Oct 2020 11:12:17 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=raphael.cauderlier AT nomadic-labs.com; spf=SoftFail smtp.mailfrom=raphael.cauderlier AT nomadic-labs.com; spf=None smtp.helo=postmaster AT redisdead.crans.org
Ironport-phdr: 9a23:M94Xpxc2q4ydbfEk0vVDOKStlGMj4u6mDksu8pMizoh2WeGdxcW+YR7h7PlgxGXEQZ/co6odzbaP7Oa9ACdZu96oizMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCybL9vLhi6twXcutQZjYd/NKo61wfErGZPd+lK321jOEidnwz75se+/Z5j9zpftvc8/MNeUqv0Yro1Q6VAADspL2466svrtQLeTQSU/XsTTn8WkhtTDAfb6hzxQ4r8vTH7tup53ymaINH2QLUpUjms86tnVBnlgzoBOjUk8m/Yl9ZwgbpVrh2vpRN/zYHbb52aOvRjYK3TfdAUSHFdXsZIUixNHp+wYpENAucHIO1Wr5P9p1wLrRamGQejHvvvyj9SiXjq2a01y/osHhvb3AM9Ad0OqnDUrNTrO6cITOu4y7PIwi/bb/NWwzjy9ozIfgo9rv6WQLJ/bNTeyVMrFwPEkFqQs5foPzWS1uQIqWeU8utgWv62h24jsQ5+uSOvyt0whYnOg4IY01bJ/jh2z4gpP9O3UlJ7YcK6H5tKsSGXL5Z6T94+Tm11uys0yrwLtJ66cSUEyZkpyRHSZvyFfoSW4hztW/ucLSl4iX9kZb6ymRm//Ei8xuHiS8W631lHoyVDn9LRuH4N0BnT5dKGSvt75kqh1jeP1xzT6uFZOk84j7bUK5kkwrM2i5EdslzDEzfrlEj1jKKabFso9+a05+j9YLjrooWQOoFwhw3mPKkjmNazDfk6PwQTRWSX5Piw2bP58UD3Q7hHiOA9nLPDv5DAP8sbo7a0Aw9L3YYn7BayFy2m38oFknkGN1JKZQyIgJL0NF3UPP/4F+2wg1K3kDtxwPDGJLLhDo3MLnjFjrjhYa5w51NfxQcz19xT+ZxZBq0bLP/xXkL9rtLVAxshPwyx2ennCdF91o0EWWKIB6+UKLnSvkWQ5uIvOeaDeosVtCzhJPc/+v7hkGE2mUUZfamow5QXcmu1HvJhI0Wce3Xjn9YBHnsTsgo6VuPlk0aCXSRPaHa1WqIw/is7B56+DYffWoCth6SM0zu8Hp1Pf2xJFlSMEWrzeIifQPcNaCeSItd7nTAeVLihTZUh1RC0uwPgxbpnNLmcxipNvpX6kdNx+uf7lBco9DUyAd7O/XuKSjROl3sITrwy64t2vEBw0FOC3LIw1+ZRDdxa6vcPWQ4nOZPGy+13Efj0XQfIctaCDVKvSM7gCjY0GIFii+QSalpwTo3xxivI2DCnVudMyu67Qacs+6eZ5EDfYsZwz3Gcjfs7glUnWcdCPGHgjbR28ROVAJTGwR3Ay/SaMJ8E1SuIz1+tiHKUtRgIAgh3VKzJXHtaYkLctpLy4UaQF+b/W4RiCRNIzIu5EoUPb9ToiVtcQ/K6aIbYZGe4l2a7QBKBzKjKZ43vKT4Q

This library might help: https://github.com/Zimmi48/transfer

> This library helps you working seamlessly with several representations for
> the same objects, switching from one to another when doing proofs and
> easily transferring theorems across representations.
--
Raphaël Cauderlier

[Coq-Club] Getting lra to work with canonical rationals, Elias Castegren, 10/08/2020
- Re: [Coq-Club] Getting lra to work with canonical rationals, Frédéric Besson, 10/08/2020
  - Re: [Coq-Club] Getting lra to work with canonical rationals, Tej Chajed, 10/08/2020
    - Re: [Coq-Club] Getting lra to work with canonical rationals, Raphaël Cauderlier, 10/09/2020
      - Re: [Coq-Club] Getting lra to work with canonical rationals, Théo Zimmermann, 10/09/2020
        
        Re: [Coq-Club] Getting lra to work with canonical rationals, Raphaël Cauderlier, 10/09/2020