diff options
| author | Hannes Schulze <haschu0103@outlook.de> | 2026-03-08 18:26:33 +0100 |
|---|---|---|
| committer | Hannes Schulze <haschu0103@outlook.de> | 2026-03-08 18:26:33 +0100 |
| commit | c290706fed69d622cfe988e732e1ad01d09e569d (patch) | |
| tree | 8822cb160e3596657fc6aa7020026d16632e8e5f /lib/Wayland/Native.lean | |
| parent | 658b74715751cb4b52b2a968325ece9a62a29fc3 (diff) | |
rework file structure
Diffstat (limited to 'lib/Wayland/Native.lean')
| -rw-r--r-- | lib/Wayland/Native.lean | 38 |
1 files changed, 17 insertions, 21 deletions
diff --git a/lib/Wayland/Native.lean b/lib/Wayland/Native.lean index 95d1739..bd85291 100644 --- a/lib/Wayland/Native.lean +++ b/lib/Wayland/Native.lean @@ -1,21 +1,27 @@ +variable {M : Type} + namespace Wayland.Native +private opaque DisplayP : NonemptyType +private opaque EventLoopP (M : Type) : NonemptyType +private opaque EventSourceP : NonemptyType + +def Display : Type := DisplayP.type +def EventLoop (M : Type) : Type := (EventLoopP M).type +def EventSource : Type := EventSourceP.type + +instance : Nonempty Display := DisplayP.property +instance : Nonempty (EventLoop M) := (EventLoopP M).property +instance : Nonempty EventSource := EventSourceP.property + @[extern "waylean_SIGINT"] -private opaque _SIGINT (u : Unit) : UInt32 +opaque SIGINT (u : Unit) : UInt32 @[extern "waylean_SIGUSR1"] -private opaque _SIGUSR1 (u : Unit) : UInt32 +opaque SIGUSR1 (u : Unit) : UInt32 @[extern "waylean_SIGUSR2"] -private opaque _SIGUSR2 (u : Unit) : UInt32 - -def SIGINT: UInt32 := _SIGINT () -def SIGUSR1: UInt32 := _SIGUSR1 () -def SIGUSR2: UInt32 := _SIGUSR2 () - -private opaque DisplayP : NonemptyType -def Display : Type := DisplayP.type -instance : Nonempty Display := DisplayP.property +opaque SIGUSR2 (u : Unit) : UInt32 @[extern "waylean_display_new"] opaque Display.new : (name : @& Option String) → IO Display @@ -23,16 +29,6 @@ opaque Display.new : (name : @& Option String) → IO Display @[extern "waylean_display_roundtrip"] opaque Display.roundtrip : (display : @& Display) → IO Unit -variable {M : Type} - -private opaque EventLoopP (M : Type) : NonemptyType -def EventLoop (M : Type) : Type := (EventLoopP M).type -instance : Nonempty (EventLoop M) := (EventLoopP M).property - -private opaque EventSourceP : NonemptyType -def EventSource : Type := EventSourceP.type -instance : Nonempty EventSource := EventSourceP.property - @[extern "waylean_event_loop_new"] opaque EventLoop.new : IO (EventLoop M) |