Documentation

Init.Data.UInt.Log2

source
@[extern lean_uint8_log2]
def UInt8.log2 (a : UInt8) :
UInt8
Equations
  • a.log2 = { val := a.val.log2 }
source
@[extern lean_uint16_log2]
def UInt16.log2 (a : UInt16) :
UInt16
Equations
  • a.log2 = { val := a.val.log2 }
source
@[extern lean_uint32_log2]
def UInt32.log2 (a : UInt32) :
UInt32
Equations
  • a.log2 = { val := a.val.log2 }
source
@[extern lean_uint64_log2]
def UInt64.log2 (a : UInt64) :
UInt64
Equations
  • a.log2 = { val := a.val.log2 }
source
@[extern lean_usize_log2]
def USize.log2 (a : USize) :
USize
Equations
  • a.log2 = { val := a.val.log2 }