idris-hackers/idris-crypto — pull request #4 by esmooov (2014-04-17 03:09:15+00:00)
Title: Fixed natToMod and implemented group-action-based modular arithmetic.

natToMod was not defined correctly in the previous commit. It would
produce the wrong result in cases where the argument wrapped the modulus
like `the (Mod 3) (natToMod 4)`. Now it works.

Implemented rotate which is equivalent to (+ (mS mZ)). Then defined
`modplus` in terms of successive rotations, recursive in the first argument,
to mimic Nat's first-argument recursion.