coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: karsar <karen.sarkisyan AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] float numbers
Date: Tue, 15 Aug 2017 14:05:25 +0800
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=karen.sarkisyan AT gmail.com; spf=Pass smtp.mailfrom=karen.sarkisyan AT gmail.com; spf=None smtp.helo=postmaster AT mail-oi0-f44.google.com
Ironport-phdr: 9a23:IQmlUhVuAW54UZwNSQO+pqh30afV8LGtZVwlr6E/grcLSJyIuqrYZRGCt8tkgFKBZ4jH8fUM07OQ6P+wHzFYqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aSV3DMl9+If2wEYrPhey20fqz8tvdeVZmnj24NLB7Ng6/t02FtcAMjI0kMa8ryRrSs3JOU+tTzGJsY1mUmkCvtY+L4Jd//nEI6Loa/MlaXPCicg==

What would be a natural choice of float number library if you want to do some

computations with floats inside Coq (like it's done for integers and nats,

I know it could be slow) , as well as reason about their properties?

It would be nice to provide a minimal example script showing how you import the library

and example of the addition of two floats as a demonstration.

Thx,

Karen

[Coq-Club] float numbers, karsar, 08/15/2017
- Re: [Coq-Club] float numbers, Laurent Thery, 08/15/2017
- Re: [Coq-Club] float numbers, Guillaume Melquiond, 08/16/2017
  - RE: [Coq-Club] float numbers, Kate Fairchild, 08/16/2017
    - Re: [Coq-Club] float numbers, karsar, 08/20/2017