git.iko.soy/Idris-dev
on master help sign in
Eq and Ord for Mod2
1115dd5Benjamin Saunders
lib/Prelude/Modular.idr+10
compare with master
unifiedsplit
@@ -45,6 +45,16 @@ public
45bitsToMod : Bits n -> Mod2 n
45bitsToMod : Bits n -> Mod2 n
46bitsToMod x = MkMod2 x
46bitsToMod x = MkMod2 x
47
47
48+instance Eq (Mod2 n) where
49+ (MkMod2 x) == (MkMod2 y) = x == y
50+
51+instance 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
57+
48instance Num (Mod2 n) where
58instance Num (Mod2 n) where
49 (+) = modAdd
59 (+) = modAdd
50 (-) = modSub
60 (-) = modSub