@@ -12,6 +12,9 @@ data Mod2 : Nat -> Type where
12modBin : (Bits n -> Bits n -> Bits n) -> Mod2 n -> Mod2 n -> Mod2 n
12modBin : (Bits n -> Bits n -> Bits n) -> Mod2 n -> Mod2 n -> Mod2 n
13modBin f (MkMod2 x) (MkMod2 y) = MkMod2 (f x y)
13modBin f (MkMod2 x) (MkMod2 y) = MkMod2 (f x y)
15+modComp : (Bits n -> Bits n -> a) -> Mod2 n -> Mod2 n -> a
16+modComp f (MkMod2 x) (MkMod2 y) = f x y
16modAdd : Mod2 n -> Mod2 n -> Mod2 n
19modAdd : Mod2 n -> Mod2 n -> Mod2 n
17modAdd = modBin bitsAdd
20modAdd = modBin bitsAdd
@@ -46,14 +49,14 @@ bitsToMod : Bits n -> Mod2 n
46bitsToMod x = MkMod2 x
49bitsToMod x = MkMod2 x
48instance Eq (Mod2 n) where
51instance Eq (Mod2 n) where
49− (MkMod2 x) == (MkMod2 y) = x == y
52+ (==) = modComp (==)
51instance Ord (Mod2 n) where
54instance Ord (Mod2 n) where
52− (MkMod2 x) > (MkMod2 y) = x > y
55+ (<) = modComp (<)
53− (MkMod2 x) >= (MkMod2 y) = x > y
56+ (<=) = modComp (<=)
54− (MkMod2 x) <= (MkMod2 y) = x > y
57+ (>=) = modComp (>=)
55− (MkMod2 x) < (MkMod2 y) = x > y
58+ (>) = modComp (>)
56− compare (MkMod2 x) (MkMod2 y) = compare x y
59+ compare = modComp compare
58instance Num (Mod2 n) where
61instance Num (Mod2 n) where
59 (+) = modAdd
62 (+) = modAdd