def Fin.log2 {m : Nat} (n : Fin m) : Fin m

Logarithm base 2 for bounded numbers.

The resulting value is the same as that computed by Nat.log2. In particular, the result for 0 is 0.

Examples:

• (8 : Fin 10).log2 = (3 : Fin 10)
• (7 : Fin 10).log2 = (2 : Fin 10)
• (4 : Fin 10).log2 = (2 : Fin 10)
• (3 : Fin 10).log2 = (1 : Fin 10)
• (1 : Fin 10).log2 = (0 : Fin 10)
• (0 : Fin 10).log2 = (0 : Fin 10)

Equations

• n.log2 = ⟨(↑n).log2, ⋯⟩