You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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).
The text was updated successfully, but these errors were encountered:
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?
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 ofFin
still has to be defined).The text was updated successfully, but these errors were encountered: