@@ -3,18 +3,23 @@ import Prelude.Bits
33
44%default total
55
6+abstract
67data Modulo : Nat -> Type where
78 MkModulo : {n : Nat} -> Bits (log2 (2*n)) -> Modulo (S n)
89
10+public
911modAdd : Modulo n -> Modulo n -> Modulo n
1012modAdd (MkModulo x) (MkModulo y) = MkModulo (bitsAdd x y)
1113
14+public
1215modSub : Modulo n -> Modulo n -> Modulo n
1316modSub (MkModulo x) (MkModulo y) = MkModulo (bitsSub x y)
1417
18+public
1519modMul : Modulo n -> Modulo n -> Modulo n
1620modMul (MkModulo x) (MkModulo y) = MkModulo (bitsMul x y)
1721
22+public
1823modDiv : Modulo n -> Modulo n -> Modulo n
1924modDiv (MkModulo x) (MkModulo y) = MkModulo (bitsUDiv x y)
2025