blob: 5212ff0c3295f7440c07b3bf3068afb9f1ebe251 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
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
|
