The position of the highest set bit of a positive natural below 2^33.
215def stdFloatFloorLog2 =
216 (lambda unrestricted value : Nat .
217 (nat-eliminate
218 (lambda unrestricted current : Nat . Nat)
219 zero
220 (lambda unrestricted position : Nat .
221 (lambda unrestricted count : Nat .
222 (nat-add count (naturalIsZero (nat-less-than value (naturalPowerOfTwo (succ position)))))))
223 32))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.