Switch to inductive binary?

[clayrat]

There's a port of inductive binary number arithmetics in the works at https://github.com/sbp/idris-bi/, which I suspect will work much faster than Fin (though the analogue of Fin still has to be defined).

[clayrat]

I'm currently doing the integers mod 2^n @idris-bi to express proofs for functions on machine bytes, which seems to be sufficient to translate the current version of this library - it only uses Mod 256 in ARC4.idr. I wonder however, if it'd be useful to implement a general mod n arithmetic as well? My guess is yes, if we would also want something like RSA or Diffie-Hellman?