Documentation

Init.Data.Nat.Log2

@[extern lean_nat_log2]

def Nat.log2 (n : Nat) :

Equations

Nat.log2 n = if n ≥ 2 then Nat.log2 (n / 2) + 1 else 0

Computes ⌊max0(log₂n)⌋.

log20=log21=0, log22=1, ..., log2(2^i)=i, etc.