coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] Why is the signature of sqrt R->R ?

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] Why is the signature of sqrt R->R ?
Date: Thu, 7 Feb 2019 14:58:37 +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.400.15
Ironport-phdr: 9a23:2kUa6x/wJMdRjv9uRHKM819IXTAuvvDOBiVQ1KB31ugcTK2v8tzYMVDF4r011RmVBdWds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+557ebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRh/2hikaKz43/mLZisJyg6JavB2uqBNxzpXIYI6OMPdyYr/Rcc8YSGdHQ81fVzZBAoS5b4YXAeYPIOFYoJfyp1sStxu+AhGsCPvywTFPh3/5wa063P4/HgHC0gArAtUDsHHVrNrpNKcdS/66zK3SwTXYaPNZxzj96JTSchAmufGBRrNwcczNyUYxEwPJlEmfqYvgPz6M0OkGrmaV7+1lVe21im4nrRl8ojmpxscwlIbJgpgZxU3a+ih/3Y07JsW4RVZmbdOqH5ZcrTyWOoV5T884Xm1ltic3xqcItJKmZCQG1ZUqyhDFZ/GJfYWE+AzvWeiVLDtimX5oe66ziw6v/UWhzuDwTNe43VZFoyZfjNXArG4B2wHX58WBV/Bz5F2u2SyV2ADW8uxEIV47la7cK5M5x74wmYAcvVjCEyPsmUX2irOWeVsg+uSy9+vnZbDmqoedN49ylA7+LrwjltGxDOk3KAQCQmaW9Oum2LH+80D0Qa9Gg/MrnqXBtZDVP8Ubpqq3Aw9P1YYj7g6yDzKn0NsEnXkINkxKeBadg4jyPFHBPv/4Deulg1SriDdm3PHGPrv9AprTKnjPiqvufbF460JE0go80chf545ICrEGOP/8RkjxtMXBAhAlNwy03v3oBc5m1oIeXGKPGrWWPLnTsV+O/OIvIvODaJUbuDbneLAZ4Kukhngg3FQZYKOB3J0NaXn+EO4saxGSZmOpidMcG08LuBA/RarkkgvRfyRUYiP4ZKUx6S0hD5riRaLCTYCkjbjLlHO+H5ZWb21CTEuLHHj0bYKcc/YKdC+WZMRml2pXBvCaV4Y92ET250fBwL19I7+Mo3xKhdfYzNFwotbru1Q3/D1wAd6a1jjUHWBygm4MATQx2fIm+BAv+hK4yaF9xsdgO5lL/foQC1U7M4LRy6pxDNWgAlucLOfMc06vR5CdOR90Tt81xIZRMUNyEo38yBHFwyeuRbQSku7TCQ==

Dear Florian,

thanks for pointing me to your multivalued-function work - it looks very
useful and appears to be designed in good ssreflect tradition.

I think since a long time to start porting pieces from Maxima to Coq, but the
design considerations are quite subtle. At some point one will need
multivalued functions, but I am not sure if this would be the best default
representation. I guess one has to really try it using various methods to see
what works best in practice.

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
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928

RE: [Coq-Club] Why is the signature of sqrt R->R ?, Soegtrop, Michael, 02/01/2019
- Re: [Coq-Club] Why is the signature of sqrt R->R ?, Théo Zimmermann, 02/01/2019
  - Re: [Coq-Club] Why is the signature of sqrt R->R ?, Florian Steinberg, 02/02/2019
    - RE: [Coq-Club] Why is the signature of sqrt R->R ?, Soegtrop, Michael, 02/04/2019
      - Re: [Coq-Club] Why is the signature of sqrt R->R ?, Richard Ford, 02/04/2019
        
        RE: [Coq-Club] Why is the signature of sqrt R->R ?, Soegtrop, Michael, 02/07/2019
      - Re: [Coq-Club] Why is the signature of sqrt R->R ?, Florian Steinberg, 02/05/2019
        
        RE: [Coq-Club] Why is the signature of sqrt R->R ?, Soegtrop, Michael, 02/07/2019