idris-hackers/idris-crypto — pull request #2 by esmooov (2014-04-15 06:03:09+00:00)
Title: Fixed finToBits using the Idris implementation of nextPow2

Data.Bits already has a nice next power of 2 function. However,
it is not exported. It should be useful for the DEA library anyway
so we import it. This fixes the problem with just using log2 for the
finToBits signature: i.e. we want a ceiling-oriented log2 function,
which is exactly what nextPow2 is.