git.iko.soy/Idris-dev
on master help sign in
Show instance for Modulo
5a26a74Benjamin Saunders
lib/Prelude.idr+3
compare with master
unifiedsplit
@@ -32,6 +32,9 @@ instance Show Nat where
32instance Show Int where
32instance Show Int where
33 show = prim__intToStr
33 show = prim__intToStr
34
34
35+instance Show (Modulo (S n)) where
36+ show = modToStr
37+
35instance Show Integer where
38instance Show Integer where
36 show = prim__bigIntToStr
39 show = prim__bigIntToStr
37
40
lib/Prelude/Modular.idr+4
@@ -23,6 +23,10 @@ public
23modDiv : Modulo n -> Modulo n -> Modulo n
23modDiv : Modulo n -> Modulo n -> Modulo n
24modDiv (MkModulo x) (MkModulo y) = MkModulo (bitsUDiv x y)
24modDiv (MkModulo x) (MkModulo y) = MkModulo (bitsUDiv x y)
25
25
26+public
27+modToStr : Modulo n -> String
28+modToStr (MkModulo x) = bitsToStr x
29+
26instance Num (Modulo (S n)) where
30instance Num (Modulo (S n)) where
27 (+) = modAdd
31 (+) = modAdd
28 (-) = modSub
32 (-) = modSub