Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Fibonacci in Coq?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Fibonacci in Coq?


Chronological Thread 
  • 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




Archive powered by MHonArc 2.6.18.

Top of Page