Documentation

Init.Data.Fin.Log2

def Fin.log2 {m : Nat} (n : Fin m) :
Fin m
Equations
  • n.log2 = (↑n).log2,
Instances For