source
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, ⋯⟩

Instances For