Documentation
Init
.
Data
.
Fin
.
Log2
Search
Google site search
Init
.
Data
.
Fin
.
Log2
source
Imports
Init.Data.Nat.Log2
Imported by
Fin
.
log2
source
def
Fin
.
log2
{m :
Nat
}
(n :
Fin
m
)
:
Fin
m
Instances For