idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-24 15:07:37 +03:00
Code Issues Projects Releases Wiki Activity

[ fix ] showTime pads nanoseconds properly (#2650)

Browse Source
This commit is contained in:
wwww 2022-09-22 04:18:26 -07:00 committed by GitHub
parent 36f930ef87
commit 38db7c3d22
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 5 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
libs/base/System/Clock.idr
View File

@ -72,12 +72,11 @@ Show (Clock type) where
export
showTime : (s, ns : Nat) -> (clk : Clock type) -> String
showTime s ns (MkClock seconds nanoseconds) =
let seconds = show seconds
quotient : Integer = cast $ 10 `power` minus 9 ns
nanoseconds = show (cast nanoseconds `div` quotient)
in concat [ padLeft s '0' seconds
, "."
, padRight ns '0' nanoseconds
let seconds' = show seconds
nanoseconds' = show nanoseconds
in concat [ padLeft s '0' seconds'
, if ns == 0 then "" else "."
, padRight ns '0' $ substr 0 ns $ (padLeft 9 '0' nanoseconds')
, "s"
]