coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Coq libraries about inverse trigonometric functions

From: Shengyi Wang <txyyss AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Coq libraries about inverse trigonometric functions
Date: Sun, 26 Jan 2020 19:13:00 +0800
Authentication-results: mail3-smtp-sop.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-vk1-f171.google.com
Ironport-phdr: 9a23:cpvkVByflLT0wxPXCy+O+j09IxM/srCxBDY+r6Qd1OgWIJqq85mqBkHD//Il1AaPAdyHrakcwLCL++C4ACpcuM3H6ChDOLV3FDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3OgV6PPn6FZDPhMqrye+y54fTYwJVjzahfL9+Nhq7oRjeu8UMj4ZuNqk9xgXJr3BVf+ha2X5kKUickhrh6Mq85oJv/zhVt/k868NOTKL2crgiQ7dFFjomKWc15MPqtRnHUwSC42YXX3sVnBRVHQXL9Qn2UZjtvCT0sOp9wzSaMtbtTb8oQzSi7rxkRwHuhSwaKjM26mDXish3jKJGvBKsogF0zoDIbI2JMvd1Y6XQds4YS2VcRMZcTyNODIOyYYUMEuQPI/pXopLnqFcStxazHxWgCP/txzJOm3T43bc60+MkEQzewQIgH8wBsHLbrNT1NacZTOC6w7POzTXMcvhb3iv96YfIcxEhuvGMRql9ccXUyUY1FgPFik+cppDiPzOQz+kAtXWQ4el4Ve+3lWIrtwV8riKsy8oskIXFmJwZxk3e+Slkwos5ONu1Q1Nhb9G+CptfrSSaOpN2Qsw8R2Fovz43yrgctp66eCgG0Yonxx3CZ/CefYiE/xDuWPuLLTd3g3Jlf72/hxKs/kS61uL8Ucy03E5LripDjNbMqmgA2wLP5sWDUPdw/Ues1SyR2wzN9+1IO104mKjGJ5I5x74/jJsTsUDNHi/sn0X2ibebdlkr++mo6+Xnea7mq4STN49xkA7+M6AultajDuQ/NwgCR3Kb9vik1L3/4U35R61HgeExkqnAqZzVOcAbprOiDAJOyYYi6xO/Dy+839gCnHkHKkhFeBOdgITzNVHOOqOwMfDqiFO11Txv2vruP7v7A5yLIGKQvq3meONG60Naxxsyhe9W4Z0cXq0RMePoQWf+sdXZClkyNAnikLWvM8l0yo5LATHHOaSeKq6H6QbZtNJqGPGFYcougBi4LvEk4/D0inpgwA0SeKCo2d0cb3XqR606cXXcWmLlh5I6KUlPphA3FbW4h1iLUDoVbHG3Dfplu2MLTbm+BIKGfbiDxbyM2CDhQM9Tb2FCT06PSDLmLtrdHfgLby2WL4lqlTlWDbU=

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