Packing trailing decimal digits into consecutive DPD declets

Trailing decimal digits are split into base-1000 groups and packed into consecutive ten-bit declets, least significant first. Decoding interprets every declet, including redundant patterns, as three decimal digits.

def FloatLib.Floats.Formats.DecimalInterchange.DPD.encodeTrailing : Nat → Nat → Nat

Pack groups base-1000 digits into consecutive ten-bit declets, least significant first.

def FloatLib.Floats.Formats.DecimalInterchange.DPD.decodeTrailing : Nat → Nat → Nat

Decode all declets, including redundant patterns, into a decimal coefficient.