git.iko.soy/Idris-dev
on master help sign in
Clean up some redundancy
88e07aaBenjamin Saunders
lib/Prelude/Modular.idr+3−11
compare with master
unifiedsplit
@@ -28,14 +28,6 @@ public
28intToMod : {n : Nat} -> Int -> Mod2 n
28intToMod : {n : Nat} -> Int -> Mod2 n
29intToMod {n=n} x = MkMod2 (intToBits x)
29intToMod {n=n} x = MkMod2 (intToBits x)
30
30
31−public
32−modToBits : Mod2 n -> Bits n
33−modToBits (MkMod2 x) = x
34−
35−public
36−bitsToMod : Bits n -> Mod2 n
37−bitsToMod x = MkMod2 x
38−
39instance Eq (Mod2 n) where
31instance Eq (Mod2 n) where
40 (==) = modComp (==)
32 (==) = modComp (==)
41
33
@@ -54,10 +46,10 @@ instance Num (Mod2 n) where
54 fromInteger = intToMod
46 fromInteger = intToMod
55
47
56instance Cast (Mod2 n) (Bits n) where
48instance Cast (Mod2 n) (Bits n) where
57− cast = modToBits
49+ cast (MkMod2 x) = x
58
50
59instance Cast (Bits n) (Mod2 n) where
51instance Cast (Bits n) (Mod2 n) where
60− cast = bitsToMod
52+ cast x = MkMod2 x
61
53
62-- TODO: Other bases
54-- TODO: Other bases
63public
55public
@@ -66,5 +58,5 @@ modToStr x = pack (reverse (helper x))
66 where
58 where
67 %assert_total
59 %assert_total
68 helper : Mod2 n -> List Char
60 helper : Mod2 n -> List Char
69− helper x = strIndex "0123456789" (bitsToInt (modToBits (x `rem` 10)))
61+ helper x = strIndex "0123456789" (bitsToInt (cast (x `rem` 10)))
70 :: (if x < 10 then [] else helper (x `div` 10))
62 :: (if x < 10 then [] else helper (x `div` 10))