idris-hackers/idris-crypto — pull request #3 by esmooov (2014-04-16 18:14:52+00:00)
Title: Fixed natToMod to successfully typecheck

Specified that unless both the Nat is (S n) and the target type is Mod (S m),
natToMod should return mZ