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

Equations

• Fin.log2 n = { val := Nat.log2 ↑n, isLt := ⋯ }