git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2895 from ziman/publish-bits
de57888Edwin Brady
libs/base/Data/Bits.idr+3
compare with master
unifiedsplit
@@ -4,6 +4,7 @@ import Data.Fin
4
4
5%default total
5%default total
6
6
7+public
7nextPow2 : Nat -> Nat
8nextPow2 : Nat -> Nat
8nextPow2 Z = Z
9nextPow2 Z = Z
9nextPow2 (S x) = if (S x) == (2 `power` l2x)
10nextPow2 (S x) = if (S x) == (2 `power` l2x)
@@ -12,9 +13,11 @@ nextPow2 (S x) = if (S x) == (2 `power` l2x)
12 where
13 where
13 l2x = log2NZ (S x) SIsNotZ
14 l2x = log2NZ (S x) SIsNotZ
14
15
16+public
15nextBytes : Nat -> Nat
17nextBytes : Nat -> Nat
16nextBytes bits = (nextPow2 (divCeilNZ bits 8 SIsNotZ))
18nextBytes bits = (nextPow2 (divCeilNZ bits 8 SIsNotZ))
17
19
20+public
18machineTy : Nat -> Type
21machineTy : Nat -> Type
19machineTy Z = Bits8
22machineTy Z = Bits8
20machineTy (S Z) = Bits16
23machineTy (S Z) = Bits16