Conversion between Dyadic and Floating

def Floating.vald (x : Floating) : Dyadic

The exact Dyadic that a Floating represents

Equations

• x.vald = Dyadic.ofIntWithPrec (↑x.n) (2 ^ 63 - x.s.toInt)

@[simp]

theorem Floating.toRat_vald (x : Floating) : x.vald.toRat = x.valq