summaryrefslogtreecommitdiff
path: root/lib/Wayland/Protocols/RiverXkbBindingsV1/Header.lean
blob: 96d0cfac72a3ec9e7ebc84abaf6af9054ad0a90c (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
27
28
29
30
31
32
33
34
35
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