Skip to Content.
Sympa Menu

coq-club - [Coq-Club] exact real arithmetic

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] exact real arithmetic


chronological Thread 
  • From: Roland Zumkeller <Roland.Zumkeller AT polytechnique.fr>
  • To: coq-club AT pauillac.inria.fr
  • Subject: [Coq-Club] exact real arithmetic
  • Date: Mon, 20 Sep 2004 12:26:58 +0200
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

I'm looking for a developement of exact real arithmetic in coq (if not available, in ml). Such a library should be able to calculate any expression up to a given precision.
This kind of real numbers are most commonly represented by infinite digit sequences or continuos fractions.
Thank you for providing any references.





Archive powered by MhonArc 2.6.16.

Top of Page