From 80317994ba8a8b7f72c0bf0d824e4ade59a4b6c8 Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Thu, 9 Apr 2026 23:07:23 +0200 Subject: fix build on linux --- .../Protocols/RiverLayerShellV1/Header.lean | 36 ++++++++++++++++++++++ 1 file changed, 36 insertions(+) create mode 100644 lib/Wayland/Protocols/RiverLayerShellV1/Header.lean (limited to 'lib/Wayland/Protocols/RiverLayerShellV1/Header.lean') diff --git a/lib/Wayland/Protocols/RiverLayerShellV1/Header.lean b/lib/Wayland/Protocols/RiverLayerShellV1/Header.lean new file mode 100644 index 0000000..7c01f90 --- /dev/null +++ b/lib/Wayland/Protocols/RiverLayerShellV1/Header.lean @@ -0,0 +1,36 @@ +import Wayland.Display + +namespace Wayland.Protocols + +abbrev RiverLayerShellV1.name : InterfaceName := "river_layer_shell_v1" +abbrev RiverLayerShellOutputV1.name : InterfaceName := "river_layer_shell_output_v1" +abbrev RiverLayerShellSeatV1.name : InterfaceName := "river_layer_shell_seat_v1" + +abbrev RiverLayerShellV1 : Type := Object RiverLayerShellV1.name +abbrev RiverLayerShellOutputV1 : Type := Object RiverLayerShellOutputV1.name +abbrev RiverLayerShellSeatV1 : Type := Object RiverLayerShellSeatV1.name + +inductive RiverLayerShellV1.Error where + | objectAlreadyCreated + +namespace RiverLayerShellV1.Error + +instance : Marshallable RiverLayerShellV1.Error where + marshal + | .int, .objectAlreadyCreated => ArgumentMarshaller.marshalInt 0 + | .uint, .objectAlreadyCreated => ArgumentMarshaller.marshalUInt 0 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .objectAlreadyCreated + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .objectAlreadyCreated + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end RiverLayerShellV1.Error + +end Wayland.Protocols \ No newline at end of file -- cgit v1.3.1