From ad2c02141844d48e9c50a05f5ce872db283751ce Mon Sep 17 00:00:00 2001
From: Hannes Schulze <haschu0103@outlook.de>
Date: Fri, 13 Mar 2026 20:10:14 +0100
Subject: type map implementation

---
 src/Waylean.lean | 29 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)

(limited to 'src/Waylean.lean')

diff --git a/src/Waylean.lean b/src/Waylean.lean
index 354b609..3565854 100644
--- a/src/Waylean.lean
+++ b/src/Waylean.lean
@@ -1,6 +1,35 @@
 import Wayland
 open Wayland
 
+
+def WLDisplay.name : InterfaceName := "wl_display"
+abbrev WLDisplay : Type := Object WLDisplay.name
+
+inductive WLDisplay.Request where
+  | sync : Request
+
+inductive WLDisplay.Event where
+  | error : Event
+  | other : Event
+
+instance : Request WLDisplay.Request where
+  messages := #[{ name := "sync", args := #[], since := 0, isDestructor := False }]
+  signature _ := sorry
+  marshal _ := do return 0
+instance : Event WLDisplay.Event where
+  messages := #[{ name := "error", args := #[.string .notNull], since := 0, isDestructor := False },
+                { name := "other", args := #[.object .nullable WLDisplay.name], since := 99, isDestructor := False}]
+  signature _ := sorry
+  demarshal _ := do return .error
+instance : Interface WLDisplay.name where
+  request := WLDisplay.Request
+  event := WLDisplay.Event
+  version := 1
+instance : ResolvedInterface WLDisplay.name where
+  referencedInterfaces := #[⟨WLDisplay.name, inferInstance⟩]
+
+
+
 structure State where
   count : Int
 
-- 
cgit v1.3.1