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.

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

Place exactly places digits after the point, padding on the left when necessary.

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.