coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coq libraries about inverse trigonometric functions

From: Shengyi Wang <txyyss AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Coq libraries about inverse trigonometric functions
Date: Sun, 26 Jan 2020 20:59:08 +0800
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=txyyss AT gmail.com; spf=Pass smtp.mailfrom=txyyss AT gmail.com; spf=None smtp.helo=postmaster AT mail-ua1-f54.google.com
Ironport-phdr: 9a23:hA44eRBqJ3ykRxlh3WQlUyQJP3N1i/DPJgcQr6AfoPdwSPv+ocbcNUDSrc9gkEXOFd2Cra4d16yN6+u8ByRAuc/H7ClZNsQUFlcssoY/p0QYGsmLCEn2frbBThcRO4B8bmJj5GyxKkNPGczzNBX4q3y26iMOSF2kbVImbuv6FZTPgMupyuu854PcYxlShDq6fLh+MAi6oR/eu8ULjoZuMKg8xgfGrnZHeuld2GdkKU6Okxrm6cq84ZBu/z5Mt/498sJLTLn3cbk/QbFEFjotLno75NfstRnNTAuP4mUTX2ALmRdWAAbL8Q/3UI7pviT1quRy1i+aPdbrTb8vQjSt871rSB7zhygZMTMy7XzahdZxjKJfpxKhugB/zovJa4ybKPZyYqXQds4cSGFcXMheSjZBD5uzYIsBDeUPPehWoYrgqVUQsRSzHhOjCP/1xzJSmnP6wa833uI8Gg/GxgwgGNcOvWzJotX1KqgSV++1zanJzT7eb/xZwzH96IfVeR0mvfGNUrJxcMrKyUk0DA7FgVCQppbkPzORzOgCr2+b7+95WO+plmUppQZxoj21ycctjInEno0VylHY9SV53YY6Pse0R1J8Yd6hFpZbqiKUN5NuT888X21lvDw2x74GtJKhYiQG1oorywTfZvGIdYWD/wjtW/yLIThigXJoYLK/iAi28Uin0uD8U9O70FdOriZcj9nDrG0B2wXd6sWHRfZx5Eih2TGI1wDc7uFLP1o4mrbcK54k2rIwl5wTvlrfHiLuhkn6kKubel8n9+Wo8ejrfKvqqoGGO4J0hQzyKqEulda+AeQ8PAgORW+b+eGk2b3/8kz4QLVLjuYtkqTCv5DaIN4Upq+9AwNPzokj7BO/Ay+80NsEhXkHME5FeBWfgof1PFHOOen0Auu7g1Sxizhm3OvGP73kApXVNHfPirbhfbBn605d0gU/195f54gHQo0Gdfn0Qwr6sMHSJh4/KQ29hej9W/tn0YZLYmKCBKCIMevtuFmHrrYzM/idf5Q9tzP0Kvxj7Pnr2yxq0WQBdLWkiMNEIEuzGe5rdh3APSjcx+wZGGJPhTIQCfTwgQTbAzFWbne2Gak742NjUd/0PcL4XomoxYe58mK7E5lRPD0UD1mNFTL1ftzBVapQLi2VJcBln3oPUr3zE9ZwhyHrjxfzzv9cFsSR/yQZsZz5090svr/ckBgz8Xp/CMHPimw=

Thank you. That is very helpful.

Shengyi Wang

Cell: +65-83509639

Laurent Thery <Laurent.Thery AT inria.fr> 于2020年1月26日周日下午7:37写道：

Hi,

there is a pull request still waiting to be merged at

https://github.com/coq/coq/pull/9803

the file you could be interested in is Ratan.v

--
Laurent

On 1/26/20 12:13 PM, Shengyi Wang wrote:
> Dear coq-clubbers,
>
> I could only find the definition and properties of arctangent in the
> standard library Coq.Reals.Ratan. I know that arccos and arcsin could be
> derived from arctan. But I wonder is there any existing libraries which
> are compatible with the current Coq standard library?
>
> Thank you very much,
>
> Shengyi Wang
>
> Cell: +65-83509639

[Coq-Club] Coq libraries about inverse trigonometric functions, Shengyi Wang, 01/26/2020
- Re: [Coq-Club] Coq libraries about inverse trigonometric functions, Laurent Thery, 01/26/2020
  - Re: [Coq-Club] Coq libraries about inverse trigonometric functions, Shengyi Wang, 01/26/2020