*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Executing real numbers as approximating functions*From*: Yannick Duchêne (Hibou57) <yannick_duchene at yahoo.fr>*Date*: Wed, 08 Aug 2012 22:50:09 +0200*Organization*: Ada @ Home*References*: <5022C259.1030709@informatik.tu-muenchen.de>*User-agent*: Opera Mail/12.01 (Linux)

Hi all, once I have heard about a formalisation to execute real numbers as approximating functions, i.e. where each real number r is implemented using a function R :: nat => float such that R n equals r approximated to the n-th digit (or something similar). Can somebody give me a reference for that? Thanks a lot, Florian

Was my two cents beside of the two other replies. -- “Syntactic sugar causes cancer of the semi-colons.” [1] “Structured Programming supports the law of the excluded muddle.” [1] [1]: Epigrams on Programming — Alan J. — P. Yale University

**References**:**[isabelle] Executing real numbers as approximating functions***From:*Florian Haftmann

- Previous by Date: Re: [isabelle] isabelle/jedit
- Next by Date: Re: [isabelle] A trick with code generation from jEdit
- Previous by Thread: Re: [isabelle] Executing real numbers as approximating functions
- Next by Thread: Re: [isabelle] Executing real numbers as approximating functions
- Cl-isabelle-users August 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list