Floating point log2

@[irreducible]

def Floating.log2 (x : Floating) : Fixed 0

n s.t. 2^n ≤ |x| < 2^(n+1), or nan

Equations

• x.log2 = bif x == 0 || x == nan || x.s == UInt64.max then nan else have a := { n := x.n.uabs.log2.toInt64 - 1 }; have b := { n := (x.s - 2 ^ 63 + 1).toInt64 }; a + b