wip tinyrwm in lean

2 files changed, 4 insertions, 14 deletions

diff --git a/lib/CWayland/CWayland.cc b/lib/CWayland/CWayland.cc
index f3c966c..08df50b 100644
--- a/lib/CWayland/CWayland.cc
+++ b/lib/CWayland/CWayland.cc
@@ -1299,17 +1299,9 @@ lean_obj_res waylean_proxy_get_type(b_lean_obj_arg proxy_obj)
     return lean_io_result_mk_ok(lean_mk_string(name));
 }
 
-// Proxy.isEqual : (x y : @& Proxy) → Bool
-lean_obj_res waylean_proxy_is_equal(b_lean_obj_arg x, b_lean_obj_arg y)
-{
-    auto x_proxy = static_cast<wl_proxy*>(lean_get_external_data(x));
-    auto y_proxy = static_cast<wl_proxy*>(lean_get_external_data(y));
-    return lean_box(x_proxy == y_proxy ? 1 : 0);
-}
-
-// Proxy.hash : (x : @& Proxy) → UInt64
-lean_obj_res waylean_proxy_hash(b_lean_obj_arg x)
+// Proxy.getID : (x : @& Proxy) → IO UInt64
+lean_obj_res waylean_proxy_get_id(b_lean_obj_arg x)
 {
     auto proxy = static_cast<wl_proxy*>(lean_get_external_data(x));
-    return lean_box_uint64(wl_proxy_get_id(proxy));
+    return lean_io_result_mk_ok(lean_box_uint64(wl_proxy_get_id(proxy)));
 }
\ No newline at end of file
diff --git a/lib/CWayland/CWayland.h b/lib/CWayland/CWayland.h
index e4a6897..ff71348 100644
--- a/lib/CWayland/CWayland.h
+++ b/lib/CWayland/CWayland.h
@@ -83,9 +83,7 @@ lean_obj_res waylean_proxy_listen          (b_lean_obj_arg proxy,
                                             lean_obj_arg   handler);
 lean_obj_res waylean_proxy_keep            (b_lean_obj_arg proxy);
 lean_obj_res waylean_proxy_get_type        (b_lean_obj_arg proxy);
-lean_obj_res waylean_proxy_is_equal        (b_lean_obj_arg x,
-                                            b_lean_obj_arg y);
-lean_obj_res waylean_proxy_hash            (b_lean_obj_arg x);
+lean_obj_res waylean_proxy_get_id          (b_lean_obj_arg x);
 
 #ifdef __cplusplus
 }