1 files changed, 26 insertions, 0 deletions
diff --git a/lib/Wayland/Basic/Duration.lean b/lib/Wayland/Basic/Duration.lean
new file mode 100644
index 0000000..5212ff0
--- /dev/null
+++ b/lib/Wayland/Basic/Duration.lean
@@ -0,0 +1,26 @@
+/-!
+# Time Durations
+
+This interface abstracts the unit of time duration values.
+-/
+
+namespace Wayland
+
+/-- A duration value. -/
+structure Duration where
+  private milliseconds : UInt32
+  deriving Repr, BEq, Inhabited
+
+def Duration.ofMilliseconds (val : UInt32) : Duration := ⟨val⟩
+def Duration.ofSeconds (val : UInt32) : Duration := .ofMilliseconds (val * 1000)
+def Duration.ofMinutes (val : UInt32) : Duration := .ofSeconds (val * 60)
+
+def Duration.toMilliseconds (val : Duration) : UInt32 := val.milliseconds
+def Duration.toSeconds (val : Duration) : UInt32 := val.toMilliseconds / 1000
+def Duration.toMinutes (val : Duration) : UInt32 := val.toSeconds / 60
+
+notation:2000 val "ms" => Duration.ofMilliseconds val
+notation:2000 val "sec" => Duration.ofSeconds val
+notation:2000 val "min" => Duration.ofMinutes val
+
+end Wayland