Publish functions needed to compute Bits indices.
commite6946d3cd6cc8658d863c5781088a8b9fdedb351
authorMatus Tejiscak <ziman@functor.sk>
dateFri 15 Jan 2016, 16:29 (11 years ago)
parent07f6ff1
libs/base/Data/Bits.idr+3
@@ -4,6 +4,7 @@ import Data.Fin
44
55%default total
66
7+public
78nextPow2 : Nat -> Nat
89nextPow2 Z = Z
910nextPow2 (S x) = if (S x) == (2 `power` l2x)
@@ -12,9 +13,11 @@ nextPow2 (S x) = if (S x) == (2 `power` l2x)
1213 where
1314 l2x = log2NZ (S x) SIsNotZ
1415
16+public
1517nextBytes : Nat -> Nat
1618nextBytes bits = (nextPow2 (divCeilNZ bits 8 SIsNotZ))
1719
20+public
1821machineTy : Nat -> Type
1922machineTy Z = Bits8
2023machineTy (S Z) = Bits16