@[extern lean_uint8_log2]

def UInt8.log2 (a : UInt8) : UInt8

@[extern lean_uint16_log2]

def UInt16.log2 (a : UInt16) : UInt16

Equations

• a.log2 = { toBitVec := { toFin := a.val.log2 } }

@[extern lean_uint32_log2]

def UInt32.log2 (a : UInt32) : UInt32

@[extern lean_uint64_log2]

def UInt64.log2 (a : UInt64) : UInt64

Equations

• a.log2 = { toBitVec := { toFin := a.val.log2 } }

@[extern lean_usize_log2]

def USize.log2 (a : USize) : USize

Equations

• a.log2 = { toBitVec := { toFin := a.val.log2 } }