not deal with seriously

decimal.idr

module decimal

record Decimal : Nat -> Type where
  MkDecimal : (places : Nat) -> (mantissa : Integer) -> Decimal places

signum : Integer -> Integer
signum n = case compare n 0 of
                LT => (-1)
                EQ => 0
                GT => 1

divRound : Integer -> Integer -> Integer
divRound n1 n2 = if (abs r * 2) >= (abs n2) then n + (signum n1) else n where
    n = n1 `div` n2
    r = n1 `mod` n2

power' : Integer -> Nat -> Integer
power' x Z = 1
power' x n = x * (x `power'` (n-1))

roundTo : (np : Nat) -> Decimal op-> Decimal np
roundTo np d = case d of
    MkDecimal op m => MkDecimal np (calc m)
  where
    divisor : Integer
    divisor = 10 `power'` (op-np)

    multiplier : Integer
    multiplier = 10 `power'` (np-op)

    calc : Integer -> Integer
    calc m = case compare np op of
                 LT => m `divRound` divisor
                 EQ => m
                 GT => m * multiplier

repl

*decimal> :let d : Decimal 3; d = MkDecimal 3 123456
*decimal> d
MkDecimal 3 123456 : Decimal 3
*decimal> mantissa d
123456 : Integer
*decimal> roundTo 2 d
MkDecimal 2 12346 : Decimal 2
*decimal> roundTo 5 d
MkDecimal 5 12345600 : Decimal 5