Cast instances for Mod2 <=> Bits and Int => Bits
commit0b96076de5ffdc74f9f5066758108ffb9bda2b9a
authorBenjamin Saunders <besaunde@sfu.ca>
dateSun 23 Dec 2012, 02:15 (14 years ago)
parentef96397
lib/Prelude/Bits.idr+3
@@ -57,6 +57,9 @@ public
5757intToBits : {n : Nat} -> Int -> Bits n
5858intToBits n = MkBits (intToBits' n)
5959
60+instance Cast Int (Bits n) where
61+ cast = intToBits
62+
6063bitsShl' : {n: Nat} -> nextBits n -> nextBits n -> nextBits n
6164bitsShl' {n=n} x c with (nextBits n)
6265 | Bits8 = pad8 n prim__shlB8 x c
lib/Prelude/Modular.idr+6
@@ -47,3 +47,9 @@ instance Num (Mod2 n) where
4747 (*) = modMul
4848 abs = id
4949 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