I just stumbled on this, and this looks very surprising to me. I would expect `N.log2_up n`

to answer the question: how many bits do I need to represent `n`

in binary, but that does not work for 1.

However, given the existence of `N.log_2_up1 : N.log2_up 1 = 0`

that seems to be done on purpose. Is there a good reason?

`Lemma log2_up_pow2 : forall a, 0<=a -> log2_up (2^a) == a.`

only works with log2_up 1 = 0

Last updated: Jun 23 2024 at 04:03 UTC