def dec.place

yaml-for-bend@0.1.1.0 · num.bend:123

import Base

123# The decimal whose digits are +ds+ (no zeros at either end) with the point
124# +point+ places from their left, written "12.5", "0.001" or "300.0". The
125# point is offset by +off+ so it can be negative.
126def dec.place(+ds: String, +point: Nat, +off: Nat) -> String:
127  +n = String.length(ds)
128  when(String, String.is_empty(ds), u => "0.0",
129    u => when(String, Nat.is_le(point, off), u => "0." ++ zeros(Nat.sub(off, point)) ++ ds,
130      u => when(String, Nat.is_ge(Nat.sub(point, off), n), u => ds ++ zeros(Nat.sub(Nat.sub(point, off), n)) ++ ".0",
131        u => String.take(ds, Nat.sub(point, off)) ++ "." ++ String.drop(ds, Nat.sub(point, off)))))