diff options
Diffstat (limited to 'lib/Wayland/Protocols/RiverXkbBindingsV1/Header.lean')
| -rw-r--r-- | lib/Wayland/Protocols/RiverXkbBindingsV1/Header.lean | 36 |
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 |
