def StrataDDM.Decimal.toRat (d : Decimal) : Rat

Equations

• d.toRat = if d.exponent < 0 then mkRat d.mantissa (10 ^ d.exponent.natAbs) else Rat.ofInt (d.mantissa * 10 ^ d.exponent.natAbs)

def StrataDDM.Decimal.fromRat (r : Rat) : Option Decimal

Convert a rational number to a decimal representation. Returns some if the rational can be exactly represented as a terminating decimal, none otherwise (denominator has factors other than 2 and 5).

Equations

• One or more equations did not get rendered due to their size.