idris-lang / Idris2

A purely functional programming language with first class types
https://idris-lang.org/
Other
2.46k stars 369 forks source link

[ base ] Move most useful and stable parts of `Data.Fin.Extra` to `base` #3304

Closed buzden closed 3 weeks ago

buzden commented 3 weeks ago

Description

(At least) I use some pieces in Data.Fin.Extra half times I use Data.Fin. Some other parts are tricky or have complicated dependencies. I propose to move some (I think) most useful parts of Data.Fin.Extra to base, splitting it to different modules to not to make clutter of Data.Fin namespace and module.

Also, I realised that one function that has been in Data.Fin.Extra for a very long time now is implemented in Data.Fin with a different name, so I suggest to deprecate definition in Data.Fin.Extra in favour of definition from base.

Also, I moved one division-related function that was in Data.Fin.Extra and left there near the other division-related functions.

For backwards compatibility, I added re-exports of newly added base modules into Data.Fin.Extra.

Should this change go in the CHANGELOG?