git.iko.soy/Idris-dev
on master help sign in
DRY
42405c8Benjamin Saunders
lib/Prelude/Modular.idr+8−5
compare with master
unifiedsplit
@@ -9,25 +9,28 @@ public
9data Mod2 : Nat -> Type where
9data Mod2 : Nat -> Type where
10 MkMod2 : {n : Nat} -> Bits n -> Mod2 n
10 MkMod2 : {n : Nat} -> Bits n -> Mod2 n
11
11
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+
12public
15public
13modAdd : Mod2 n -> Mod2 n -> Mod2 n
16modAdd : Mod2 n -> Mod2 n -> Mod2 n
14−modAdd (MkMod2 x) (MkMod2 y) = MkMod2 (bitsAdd x y)
17+modAdd = modBin bitsAdd
15
18
16public
19public
17modSub : Mod2 n -> Mod2 n -> Mod2 n
20modSub : Mod2 n -> Mod2 n -> Mod2 n
18−modSub (MkMod2 x) (MkMod2 y) = MkMod2 (bitsSub x y)
21+modSub = modBin bitsSub
19
22
20public
23public
21modMul : Mod2 n -> Mod2 n -> Mod2 n
24modMul : Mod2 n -> Mod2 n -> Mod2 n
22−modMul (MkMod2 x) (MkMod2 y) = MkMod2 (bitsMul x y)
25+modMul = modBin bitsMul
23
26
24public partial
27public partial
25modDiv : Mod2 n -> Mod2 n -> Mod2 n
28modDiv : Mod2 n -> Mod2 n -> Mod2 n
26−modDiv (MkMod2 x) (MkMod2 y) = MkMod2 (bitsUDiv x y)
29+modDiv = modBin bitsUDiv
27
30
28public partial
31public partial
29modRem : Mod2 n -> Mod2 n -> Mod2 n
32modRem : Mod2 n -> Mod2 n -> Mod2 n
30−modRem (MkMod2 x) (MkMod2 y) = MkMod2 (bitsURem x y)
33+modRem = modBin bitsSDiv
31
34
32%assert_total
35%assert_total
33public
36public