Merge pull request #2895 from ziman/publish-bits
Publish functions needed to compute the index of Bits
commitde57888e374d83e83c07bd0f669d08f235b6f512
authorEdwin Brady <edwin.brady@gmail.com>
dateWed 20 Jan 2016, 16:13 (11 years ago)
parent23c2788e6946d3
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