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:51:00 +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 mga17.intel.com
Dlp-product: dlpe-windows
Dlp-reaction: no-action
Dlp-version: 11.0.400.15
Ironport-phdr: 9a23:CixAkxXq2gdq1+A2BM67zBdj0+fV8LGtZVwlr6E/grcLSJyIuqrYbBKDt8tkgFKBZ4jH8fUM07OQ7/iwHzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba9xIRmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmijoINyQh/W/XlMJ+kb5brhyiqRxxwYHUYZ2aO/Vlc6zHYd8XQXBMUtpNWyFDBI63cosBD/AGPeZdt4TxqUYArRygCgmjGOPv0DhIhmfu0aYn1OohEB3J3Aw6EN0QtHTYosj+OaAXUeC00KbIzS/MYO1S2Tvn84jIdQ4uof6QXbJqdsrR0VIiFwLDjlWMt4PlOymZ2fgKs2ie9udtU/+khWAgqwF0uDevx8Esh5HIhoIT0FDE9D92zJw7Jd2iUEJ7YNikEIdOuCGeLYd5X90tTmd1syg50r0LoYO3cSwUxJg9xxPSa+aLfoiW7h75SeqcISp0iGp4dL++iRu+60atx+PmWsWq3ltHqjBJnsTPu3wRzxDf98mKR/9n8ku/2TuC2Brf5v9eLUwqiKbWL5gsyaMqmJUJq0TMBCr2lV32jKCIckUk/fCl6+HoYrr8u5ORNZV4igD4MqQyhMO/Bf40PRQJX2ie4ei81bvj8lPlQLhSk/E7lrfVvIraKMkbvKK0AxFZ3pw+5xu/EjuqyNEYkmMGLFJBdhKHlY/pO1TWLfD9DPewn1Ssny11yPDCJLHhGZLNIWbMkLf9Z7Z97FZcxREyzdBZ+5JbFLUBLOjvVU/2sdzUFgU5PBCsw+b7FNV90ZsTVn6IAq+AKa/drVuI5v80LOSXf48UuDP9K+A/6PL0jH85n0Udfaiz0pcNZnC4BKcuH0LMK3Hrm5IKFXoAlgs4Vu3jzlOYG3YHbHGrGqk4+zsTCYS8DI6FSJr705Kb2yLuVKZRa29aEFeUVT/Ndo6EUvoIImrGJ85qkjUJUf66TIIuyQuprCf7zaZqKqzf/ShO5sGr78R8++CGzUJ6zjdzFcnIizjcHVExpXsBQnoN5I46pEV8zlmZ1q0h2q5ZE8Be47VCVQJobMeAndw/MMj7X0f6RvnMUEyvG4z0ADctQ9Z3yNgLMR4kRoeSyyvb1i/vOIc70ryGAJttrfDZ0HGoeIB8zWrL0O8qiFx0GsY=

Dear Rich,

I wonder if you have investigated Coquelicot (http://coquelicot.saclay.inria.fr/)?

so far I used Coquelicot mostly indirectly via tools which use it (like CoqInterval), but I guess it is time to re-read the corresponding chapters in the book and to re-visit the topic.

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