create Moment.now

sullyj3 · Aug 4, 2024 · 6188d56 · 6188d56
1 parent 1a23f39
commit 6188d56
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 1 deletion.
diff --git 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
@@ -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