Double IEEE constants: infinity, NaN, epsilon ... where are they?

[edwinb]

Issue by nicolabotta
Tuesday Oct 29, 2019 at 07:48 GMT
Originally opened as edwinb/Idris2-boot#146

---

Is there a way of accessing these values in Idris 2? Something like Numeric.IEEEin Haskell? At lest epsilon, infinity and NaN are badly needed, e.g., to implement interval arithmetics! Thanks, Nicola

[edwinb]

Comment by edwinb
Saturday Dec 07, 2019 at 15:13 GMT

---

I've labelled this with "Feature request" - we ought to have them really. If anyone wants pointers on where to start implementing it, please let me know.

[mr-infty]

@edwinb I'd like to start contributing to Idris 2 and I find this issue interesting. Could you give me a hint on where to start?

[ohad]

I think the right places to start would be:

libs/prelude/Prelude/Num.idr

where you'll need to add binding for the primitive constants, and also the places where the primitives are defined, e.g.

support/chez/support.ss

where you'll need to define primitive Scheme / Racket primitives to bind to.

[melted]

The primitives should be defined in support/chez/support.ss (and racket and gambit), if needed (they might not need anything but what's put out in codegen). The bootstrap files shouldn't have to be updated by hand.

[ohad]

Ah, sorry for misleading. I've removed my incorrect text.

[mr-infty]

@ohad @melted Thanks for your help!