@@ -9,25 +9,28 @@ public
99data Mod2 : Nat -> Type where
1010 MkMod2 : {n : Nat} -> Bits n -> Mod2 n
1111
12+modBin : (Bits n -> Bits n -> Bits n) -> Mod2 n -> Mod2 n -> Mod2 n
13+modBin f (MkMod2 x) (MkMod2 y) = MkMod2 (f x y)
14+
1215public
1316modAdd : Mod2 n -> Mod2 n -> Mod2 n
14−modAdd (MkMod2 x) (MkMod2 y) = MkMod2 (bitsAdd x y)
17+modAdd = modBin bitsAdd
1518
1619public
1720modSub : Mod2 n -> Mod2 n -> Mod2 n
18−modSub (MkMod2 x) (MkMod2 y) = MkMod2 (bitsSub x y)
21+modSub = modBin bitsSub
1922
2023public
2124modMul : Mod2 n -> Mod2 n -> Mod2 n
22−modMul (MkMod2 x) (MkMod2 y) = MkMod2 (bitsMul x y)
25+modMul = modBin bitsMul
2326
2427public partial
2528modDiv : Mod2 n -> Mod2 n -> Mod2 n
26−modDiv (MkMod2 x) (MkMod2 y) = MkMod2 (bitsUDiv x y)
29+modDiv = modBin bitsUDiv
2730
2831public partial
2932modRem : Mod2 n -> Mod2 n -> Mod2 n
30−modRem (MkMod2 x) (MkMod2 y) = MkMod2 (bitsURem x y)
33+modRem = modBin bitsSDiv
3134
3235%assert_total
3336public