[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: representing reals

R.W.Butler@larc.nasa.gov wrote:
> We have a library for reals/analysis at Langley's web site
>   http://atb-www.larc.nasa.gov/ftp/larc/PVS-library/
> but there are no special means provided for creating "constant" reals.
> There are functions like sqrt and exp that could be used for
> contructing irrationals.  What real numbers are you in need of?
> The analysis library includes differentiation but integrals are not
> defined, so more exotic reals will not be achievable with this library.
> Rick Butler

You can also use the library to define the reals you want
as limits of sequences or as solutions of equations.

Bruno Dutertre