Documentation

Init.Data.Fin.Log2

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