Function vstd::arithmetic::logarithm::log

source ·

pub open spec fn log(base: int, pow: int) -> int

Expand description

recommends

base > 1,

pow >= 0,

{
    if pow < base || pow / base >= pow || pow / base < 0 {
        0
    } else {
        1 + log(base, pow / base)
    }
}

This function recursively defines the integer logarithm. It’s only meaningful when the base of the logarithm base is greater than 1, and when the value whose logarithm is taken, pow, is non-negative.