Add bindings for numeric typeclasses

agda / agda2hs

Compiling Agda code to readable Haskell

https://agda.github.io/agda2hs

MIT License

176 stars 37 forks source link

Add bindings for numeric typeclasses #262

Open jespercockx opened 9 months ago

jespercockx commented 9 months ago

Currently we are missing support for the following classes:

[ ] Real
[ ] Integral
[ ] Fractional
[ ] Floating
[ ] RealFrac
[ ] RealFloat

For everything up to and including Fractional we could be able to give definitions on the Agda side (or steal them from the standard library). For the rest, we should probably just postulate them.

ndcroos commented 3 months ago

Hi, I'd like to work on this. Can you assign it to me, please? Should a file be created for each of these numeric typeclasses, in lib/Haskell/Prim?

jespercockx commented 3 months ago

Thank you, assigned! I think having one file per typeclass makes sense, yeah.