@[extern lean_uint8_log2]

def UInt8.log2 (a : UInt8) : UInt8

Equations

• UInt8.log2 a = { val := Fin.log2 a.val }

@[extern lean_uint16_log2]

def UInt16.log2 (a : UInt16) : UInt16

Equations

• UInt16.log2 a = { val := Fin.log2 a.val }

@[extern lean_uint32_log2]

def UInt32.log2 (a : UInt32) : UInt32

Equations

• UInt32.log2 a = { val := Fin.log2 a.val }

@[extern lean_uint64_log2]

def UInt64.log2 (a : UInt64) : UInt64

Equations

• UInt64.log2 a = { val := Fin.log2 a.val }

@[extern lean_usize_log2]

def USize.log2 (a : USize) : USize

Equations

• USize.log2 a = { val := Fin.log2 a.val }