diff --git a/src/Sand/SandDaemon/HandleCommand.lean b/src/Sand/SandDaemon/HandleCommand.lean index 85eb27e..b191350 100644 --- a/src/Sand/SandDaemon/HandleCommand.lean +++ b/src/Sand/SandDaemon/HandleCommand.lean @@ -69,7 +69,7 @@ private partial def countdown (id : TimerId) (due : Moment) : CmdHandlerT IO Uni loop where loop := do - let now ← Moment.mk <$> IO.monoMsNow + let now ← Moment.now let remaining := due - now -- This task will be cancelled if the timer is cancelled or paused. -- in case of resumed, a new separate task will be spawned. diff --git a/src/Sand/Time.lean b/src/Sand/Time.lean index 29bcc28..d2ff712 100644 --- a/src/Sand/Time.lean +++ b/src/Sand/Time.lean @@ -8,6 +8,8 @@ structure Moment where millis : Nat deriving Repr, ToJson, FromJson, BEq +def Moment.now : IO Moment := Moment.mk <$> IO.monoMsNow + structure Duration where millis : Nat deriving Repr, ToJson, FromJson, BEq