@@ -12,6 +12,9 @@ data Mod2 : Nat -> Type where
1212modBin : (Bits n -> Bits n -> Bits n) -> Mod2 n -> Mod2 n -> Mod2 n
1313modBin f (MkMod2 x) (MkMod2 y) = MkMod2 (f x y)
1414
15+modComp : (Bits n -> Bits n -> a) -> Mod2 n -> Mod2 n -> a
16+modComp f (MkMod2 x) (MkMod2 y) = f x y
17+
1518public
1619modAdd : Mod2 n -> Mod2 n -> Mod2 n
1720modAdd = modBin bitsAdd
@@ -46,14 +49,14 @@ bitsToMod : Bits n -> Mod2 n
4649bitsToMod x = MkMod2 x
4750
4851instance Eq (Mod2 n) where
49− (MkMod2 x) == (MkMod2 y) = x == y
52+ (==) = modComp (==)
5053
5154instance Ord (Mod2 n) where
52− (MkMod2 x) > (MkMod2 y) = x > y
53− (MkMod2 x) >= (MkMod2 y) = x > y
54− (MkMod2 x) <= (MkMod2 y) = x > y
55− (MkMod2 x) < (MkMod2 y) = x > y
56− compare (MkMod2 x) (MkMod2 y) = compare x y
55+ (<) = modComp (<)
56+ (<=) = modComp (<=)
57+ (>=) = modComp (>=)
58+ (>) = modComp (>)
59+ compare = modComp compare
5760
5861instance Num (Mod2 n) where
5962 (+) = modAdd