git.iko.soy/Idris-dev
on master help sign in
Access qualifiers for Modulo
279b02dBenjamin Saunders
lib/Prelude/Modular.idr+5
compare with master
unifiedsplit
@@ -3,18 +3,23 @@ import Prelude.Bits
3
3
4%default total
4%default total
5
5
6+abstract
6data Modulo : Nat -> Type where
7data Modulo : Nat -> Type where
7 MkModulo : {n : Nat} -> Bits (log2 (2*n)) -> Modulo (S n)
8 MkModulo : {n : Nat} -> Bits (log2 (2*n)) -> Modulo (S n)
8
9
10+public
9modAdd : Modulo n -> Modulo n -> Modulo n
11modAdd : Modulo n -> Modulo n -> Modulo n
10modAdd (MkModulo x) (MkModulo y) = MkModulo (bitsAdd x y)
12modAdd (MkModulo x) (MkModulo y) = MkModulo (bitsAdd x y)
11
13
14+public
12modSub : Modulo n -> Modulo n -> Modulo n
15modSub : Modulo n -> Modulo n -> Modulo n
13modSub (MkModulo x) (MkModulo y) = MkModulo (bitsSub x y)
16modSub (MkModulo x) (MkModulo y) = MkModulo (bitsSub x y)
14
17
18+public
15modMul : Modulo n -> Modulo n -> Modulo n
19modMul : Modulo n -> Modulo n -> Modulo n
16modMul (MkModulo x) (MkModulo y) = MkModulo (bitsMul x y)
20modMul (MkModulo x) (MkModulo y) = MkModulo (bitsMul x y)
17
21
22+public
18modDiv : Modulo n -> Modulo n -> Modulo n
23modDiv : Modulo n -> Modulo n -> Modulo n
19modDiv (MkModulo x) (MkModulo y) = MkModulo (bitsUDiv x y)
24modDiv (MkModulo x) (MkModulo y) = MkModulo (bitsUDiv x y)
20
25