type map implementation

1 files changed, 29 insertions, 0 deletions

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