coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] flooring a real number in Coq

From: Daniel Schepler <dschepler AT gmail.com>
To: coq-club AT inria.fr, "Lucian M. Patcas" <lucian.patcas AT gmail.com>
Subject: Re: [Coq-Club] flooring a real number in Coq
Date: Tue, 24 Sep 2013 19:25:56 -0700

On Tuesday, September 24, 2013 09:20:22 PM Lucian M. Patcas wrote:
> Hello,
>
> I couldn't find a floor function for real numbers in the Standard Library.
> Is anyone aware of such a function in other libraries?

Well, according to the axiom archimed, 0 < IZR (up r) - r <= 1, so I guess
you
could define Rfloor x := (up x - 1)%Z.
--
Daniel Schepler

[Coq-Club] flooring a real number in Coq, Lucian M. Patcas, 09/25/2013
- Re: [Coq-Club] flooring a real number in Coq, Daniel Schepler, 09/25/2013