summaryrefslogtreecommitdiff
path: root/lib/Wayland/Display.lean
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Wayland/Display.lean')
-rw-r--r--lib/Wayland/Display.lean12
1 files changed, 12 insertions, 0 deletions
diff --git a/lib/Wayland/Display.lean b/lib/Wayland/Display.lean
index 704d7d4..3cfa679 100644
--- a/lib/Wayland/Display.lean
+++ b/lib/Wayland/Display.lean
@@ -416,6 +416,18 @@ def DisplayM.getDisplay' : DisplayM σ (Object "wl_display") := do
variable {ι ι' : InterfaceName}
+instance : BEq (Object ι) where
+ beq x y := x.proxy.isEqual y.proxy
+
+instance : Hashable (Object ι) where
+ hash x := x.proxy.hash
+
+instance : BEq AnyObject where
+ beq x y := x.proxy.isEqual y.proxy
+
+instance : Hashable AnyObject where
+ hash x := x.proxy.hash
+
private def marshalArguments (marshaller : ∀ {α} [ArgumentMarshaller α], α OpCode) : IO (Native.ArgumentBuffer × OpCode) := do
let argBuffer ← Native.ArgumentBuffer.new
let opcode : Except String OpCode ← ArgumentBufferM.run (ExceptT.run marshaller) argBuffer