From 3d722b15a21977931a0bfa99bd8c6a235682a6d9 Mon Sep 17 00:00:00 2001
From: Hannes Schulze <contact@haschu.me>
Date: Sat, 11 Apr 2026 19:43:29 +0200
Subject: start implementing wm

---
 lib/Wayland/Display.lean | 12 ++++++++++++
 lib/Wayland/Native.lean  |  6 ++++++
 2 files changed, 18 insertions(+)

(limited to 'lib/Wayland')

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
diff --git a/lib/Wayland/Native.lean b/lib/Wayland/Native.lean
index b4e9e95..601c709 100644
--- a/lib/Wayland/Native.lean
+++ b/lib/Wayland/Native.lean
@@ -142,4 +142,10 @@ opaque Proxy.keep : (proxy : @& Proxy) → IO Unit
 @[extern "waylean_proxy_get_type"]
 opaque Proxy.getType : (proxy : @& Proxy) → IO String
 
+@[extern "waylean_proxy_is_equal"]
+opaque Proxy.isEqual : (x y : @& Proxy) → Bool
+
+@[extern "waylean_proxy_hash"]
+opaque Proxy.hash : (x : @& Proxy) → UInt64
+
 end Wayland.Native
-- 
cgit v1.3.1