summaryrefslogtreecommitdiff
path: root/lib/Wayland/Protocols/RiverXkbBindingsV1/Header.lean
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Wayland/Protocols/RiverXkbBindingsV1/Header.lean')
-rw-r--r--lib/Wayland/Protocols/RiverXkbBindingsV1/Header.lean36
1 files changed, 36 insertions, 0 deletions
diff --git a/lib/Wayland/Protocols/RiverXkbBindingsV1/Header.lean b/lib/Wayland/Protocols/RiverXkbBindingsV1/Header.lean
new file mode 100644
index 0000000..96d0cfa
--- /dev/null
+++ b/lib/Wayland/Protocols/RiverXkbBindingsV1/Header.lean
@@ -0,0 +1,36 @@
+import Wayland.Display
+
+namespace Wayland.Protocols
+
+abbrev RiverXkbBindingsV1.name : InterfaceName := "river_xkb_bindings_v1"
+abbrev RiverXkbBindingV1.name : InterfaceName := "river_xkb_binding_v1"
+abbrev RiverXkbBindingsSeatV1.name : InterfaceName := "river_xkb_bindings_seat_v1"
+
+abbrev RiverXkbBindingsV1 : Type := Object RiverXkbBindingsV1.name
+abbrev RiverXkbBindingV1 : Type := Object RiverXkbBindingV1.name
+abbrev RiverXkbBindingsSeatV1 : Type := Object RiverXkbBindingsSeatV1.name
+
+inductive RiverXkbBindingsV1.Error where
+ | objectAlreadyCreated
+
+namespace RiverXkbBindingsV1.Error
+
+instance : Marshallable RiverXkbBindingsV1.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 RiverXkbBindingsV1.Error
+
+end Wayland.Protocols \ No newline at end of file