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

Equations

• Fin.log2 n = { val := Nat.log2 n.val, isLt := (_ : Nat.log2 n.val < m) }