Documentation
Init
.
Data
.
UInt
.
Log2
Search
Google site search
Init
.
Data
.
UInt
.
Log2
source
Imports
Init.Data.Fin.Log2
Imported by
UInt8
.
log2
UInt16
.
log2
UInt32
.
log2
UInt64
.
log2
USize
.
log2
source
@[extern lean_uint8_log2]
def
UInt8
.
log2
(a :
UInt8
)
:
UInt8
Instances For
source
@[extern lean_uint16_log2]
def
UInt16
.
log2
(a :
UInt16
)
:
UInt16
Instances For
source
@[extern lean_uint32_log2]
def
UInt32
.
log2
(a :
UInt32
)
:
UInt32
Instances For
source
@[extern lean_uint64_log2]
def
UInt64
.
log2
(a :
UInt64
)
:
UInt64
Instances For
source
@[extern lean_usize_log2]
def
USize
.
log2
(a :
USize
)
:
USize
Instances For