on master help sign in
Remove unused utility function
dfb6802Benjamin Saunders
lib/Prelude/Bits.idr−6
@@ -64,12 +64,6 @@ pad64' n f x y = prim__lshrB64 (f (prim__shlB64 x pad) y) pad
64 where
64 where
65 pad = (prim__intToB64 (cast (64-n)))
65 pad = (prim__intToB64 (cast (64-n)))
66
66
67−%assert_total
68−pow : Int -> Int -> Int
69−pow x y = if y > 0
70− then x * (pow x (y - 1))
71− else 1
72−
73%assert_total
67%assert_total
74intToBits' : Int -> machineTy (log2Bytes n)
68intToBits' : Int -> machineTy (log2Bytes n)
75intToBits' {n=n} x with (log2Bytes n)
69intToBits' {n=n} x with (log2Bytes n)