HepLean Documentation
Init
.
Data
.
UInt
.
Log2
Search
Google site search
return to top
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
Equations
a
.log2
=
{
toBitVec
:=
{
toFin
:=
a
.val
.log2
}
}
Instances For
source
@[extern lean_uint16_log2]
def
UInt16
.
log2
(a :
UInt16
)
:
UInt16
Equations
a
.log2
=
{
toBitVec
:=
{
toFin
:=
a
.val
.log2
}
}
Instances For
source
@[extern lean_uint32_log2]
def
UInt32
.
log2
(a :
UInt32
)
:
UInt32
Equations
a
.log2
=
{
toBitVec
:=
{
toFin
:=
a
.val
.log2
}
}
Instances For
source
@[extern lean_uint64_log2]
def
UInt64
.
log2
(a :
UInt64
)
:
UInt64
Equations
a
.log2
=
{
toBitVec
:=
{
toFin
:=
a
.val
.log2
}
}
Instances For
source
@[extern lean_usize_log2]
def
USize
.
log2
(a :
USize
)
:
USize
Equations
a
.log2
=
{
toBitVec
:=
{
toFin
:=
a
.val
.log2
}
}
Instances For