From c290706fed69d622cfe988e732e1ad01d09e569d Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Sun, 8 Mar 2026 18:26:33 +0100 Subject: rework file structure --- lib/Wayland/Basic/Duration.lean | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) create mode 100644 lib/Wayland/Basic/Duration.lean (limited to 'lib/Wayland/Basic/Duration.lean') 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 -- cgit v1.3.1