@@ -28,14 +28,6 @@ public
2828intToMod : {n : Nat} -> Int -> Mod2 n
2929intToMod {n=n} x = MkMod2 (intToBits x)
3030
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−
3931instance Eq (Mod2 n) where
4032 (==) = modComp (==)
4133
@@ -54,10 +46,10 @@ instance Num (Mod2 n) where
5446 fromInteger = intToMod
5547
5648instance Cast (Mod2 n) (Bits n) where
57− cast = modToBits
49+ cast (MkMod2 x) = x
5850
5951instance Cast (Bits n) (Mod2 n) where
60− cast = bitsToMod
52+ cast x = MkMod2 x
6153
6254-- TODO: Other bases
6355public
@@ -66,5 +58,5 @@ modToStr x = pack (reverse (helper x))
6658 where
6759 %assert_total
6860 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)))
7062 :: (if x < 10 then [] else helper (x `div` 10))