[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