coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Kenneth Adam Miller <kennethadammiller AT gmail.com>
- To: coq-club Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Fibonacci in Coq?
- Date: Fri, 27 Oct 2017 11:23:41 -0400
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=kennethadammiller AT gmail.com; spf=Pass smtp.mailfrom=kennethadammiller AT gmail.com; spf=None smtp.helo=postmaster AT mail-lf0-f53.google.com
- Ironport-phdr: 9a23:TKVPeRbDViYTAePHS4Wj1rT/LSx+4OfEezUN459isYplN5qZpcyybnLW6fgltlLVR4KTs6sC0LWG9f24EUU7or+/81k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i76xXcoFx7+LQt4IPjuUs6X1pzvlrP6x5qGaAJRwTG5fLk6BxGrp02Fvc4PxIBmN6wZyx3To3IOdf4Alk1yIlfGvBv64Mqs/NZK/y1V89cg88pNS+2ufKk+S7FEDD0qOmUw5cnvuAPrQg6G539aWWITxEkbSzPZ5Q33C8+i+hDxsfBwjWzDZZX7
Cool thanks!
I'm looking for analytic continuations of the continuous series as well as an alternative to starting at zero, and lastly some theoretic derivations of it's convergence point, with the work shown.
On Fri, Oct 27, 2017 at 2:51 AM, Laurent Thery <Laurent.Thery AT inria.fr> wrote:
On 10/26/2017 09:44 PM, Kenneth Adam Miller wrote:
> Hello,
>
> Does anybody know of any theorems or number theoretic work done using
> fibonacci in Coq?
>
> Thanks in advance!
I don't know which results you have in mind. The mathcomp has only some
basic properties of the fib function
https://github.com/math-comp/math-comp/blob/master/mathcomp/attic/fib.v
--
Laurent
Ps: fib.v is not part of the standard mathcomp library
- [Coq-Club] Fibonacci in Coq?, Kenneth Adam Miller, 10/26/2017
- Re: [Coq-Club] Fibonacci in Coq?, Laurent Thery, 10/27/2017
- Re: [Coq-Club] Fibonacci in Coq?, Kenneth Adam Miller, 10/27/2017
- Re: [Coq-Club] Fibonacci in Coq?, Pierre Letouzey, 10/27/2017
- Re: [Coq-Club] Fibonacci in Coq?, Kenneth Adam Miller, 10/27/2017
- Re: [Coq-Club] Fibonacci in Coq?, Pierre Letouzey, 10/27/2017
- Re: [Coq-Club] Fibonacci in Coq?, Kenneth Adam Miller, 10/27/2017
- Re: [Coq-Club] Fibonacci in Coq?, Laurent Thery, 10/27/2017
Archive powered by MHonArc 2.6.18.