Fixed and scientific decimal presentation

These renderers place the decimal point in the digits of an exact decimal record. They perform no rounding and retain coefficient trailing zeros. Scientific notation keeps one digit before the point and always prints an exponent, including for signed zero.

formatDyadicCompact is the exception: it first removes fractional trailing zeros, then prints fixed notation such as 1.5 or 6, falling back to the shorter e exponent form when fixed notation would need more characters. It is the text of a Dyadic. ofRat? gives the exact decimal record of a rational with a terminating expansion.

def FloatLib.Numerics.DecimalText.pointCharacters (whole fraction : List Char) : List Char

Join whole and fractional digits, omitting the point when there are no fractional digits.

def FloatLib.Numerics.DecimalText.fractionalCharacters (coefficient places : ℕ) : List Char

Write coefficient with places digits after the point, padding with zeros on the left.

def FloatLib.Numerics.DecimalText.Decimal.fixedRepresentation (value : Decimal) : Decimal

The record recovered from fixed notation: positive powers of ten become integer digits.

def FloatLib.Numerics.DecimalText.Decimal.fixedCharacters (value : Decimal) : List Char

Fixed notation with the original sign and all fractional places specified by the exponent.

def FloatLib.Numerics.DecimalText.Decimal.formatFixed (value : Decimal) : String

Fixed decimal text, with no precision limit or additional rounding.

def FloatLib.Numerics.DecimalText.Decimal.scientificCharacters (value : Decimal) : List Char

Scientific notation with one leading digit and the original coefficient's trailing zeros. For zero with exponent -places, print places fractional zeros and exponent zero. Every output determines the original decimal record, including its sign and zero precision.

def FloatLib.Numerics.DecimalText.Decimal.formatScientific (value : Decimal) : String

Scientific decimal text, with no precision limit or additional rounding.

def FloatLib.Numerics.DecimalText.Decimal.trimTrailingZerosLoop : ℕ → Decimal → Decimal

Fuel-bounded worker that removes one trailing decimal zero per step while the exponent is negative.

def FloatLib.Numerics.DecimalText.Decimal.trimTrailingZeros (value : Decimal) : Decimal

Remove fractional trailing zeros from the significand without changing the exact value. Nonnegative exponents are left alone, so integers keep their digits.

def FloatLib.Numerics.DecimalText.Decimal.compactLoop : ℕ → Decimal → Decimal

Fuel-bounded worker that moves one trailing decimal zero of a nonzero significand into the exponent per step.

def FloatLib.Numerics.DecimalText.Decimal.compact (value : Decimal) : Decimal

Move every trailing decimal zero of a nonzero significand into the exponent, so the significand has no trailing zeros. The value and sign are unchanged.

def FloatLib.Numerics.DecimalText.formatDyadicCompact (value : Dyadic) : String

Exact decimal text of a dyadic without redundant fractional zeros. Fixed notation such as 1.5 is used unless the e exponent form is shorter.

@[instance_reducible]

instance FloatLib.Numerics.DecimalText.instToStringDyadic : ToString Dyadic

Text of a dyadic: its exact value, as formatDyadicCompact writes it.

def FloatLib.Numerics.DecimalText.removeFactor (p : ℕ) : ℕ → ℕ → ℕ → ℕ × ℕ

Remove factors p from n while it is divisible, counting them, with fuel.

def FloatLib.Numerics.DecimalText.ofRat? (value : ℚ) : Option Decimal

The exact decimal record of a rational whose denominator has no prime factor other than two and five. Every other rational has a nonterminating decimal expansion and gives none.