git.iko.soy/Idris-dev
on master help sign in
Cast instances for Mod2 <=> Bits and Int => Bits
0b96076Benjamin Saunders
lib/Prelude/Bits.idr+3
compare with master
unifiedsplit
@@ -57,6 +57,9 @@ public
57intToBits : {n : Nat} -> Int -> Bits n
57intToBits : {n : Nat} -> Int -> Bits n
58intToBits n = MkBits (intToBits' n)
58intToBits n = MkBits (intToBits' n)
59
59
60+instance Cast Int (Bits n) where
61+ cast = intToBits
62+
60bitsShl' : {n: Nat} -> nextBits n -> nextBits n -> nextBits n
63bitsShl' : {n: Nat} -> nextBits n -> nextBits n -> nextBits n
61bitsShl' {n=n} x c with (nextBits n)
64bitsShl' {n=n} x c with (nextBits n)
62 | Bits8 = pad8 n prim__shlB8 x c
65 | Bits8 = pad8 n prim__shlB8 x c
lib/Prelude/Modular.idr+6
@@ -47,3 +47,9 @@ instance Num (Mod2 n) where
47 (*) = modMul
47 (*) = modMul
48 abs = id
48 abs = id
49 fromInteger = intToMod
49 fromInteger = intToMod
50+
51+instance Cast (Mod2 n) (Bits n) where
52+ cast = modToBits
53+
54+instance Cast (Bits n) (Mod2 n) where
55+ cast = bitsToMod