Rational Numbers and Float

def Rat.toFloat (a : Rat) : Float

Convert this rational number to a Float value.

Equations

• a.toFloat = a.num.divFloat ↑a.den

def Float.toRat? (a : Float) : Option Rat

Convert this floating point number to a rational value.

Equations

• a.toRat? = Option.map (fun (x : Int × Int) => match x with | (v, exp) => mkRat (v.sign * ↑(v.natAbs <<< exp.toNat)) (1 <<< (-exp).toNat)) a.toRatParts

def Float.toRat0 (a : Float) : Rat

Convert this floating point number to a rational value, mapping non-finite values (inf, -inf, nan) to 0.

Equations

• a.toRat0 = a.toRat?.getD 0

@[implicit_reducible]

instance Rat.instCoeFloat_batteries : Coe Rat Float

Equations

• Rat.instCoeFloat_batteries = { coe := Rat.toFloat }