summaryrefslogtreecommitdiff
path: root/src/Waylean.lean
diff options
context:
space:
mode:
Diffstat (limited to 'src/Waylean.lean')
-rw-r--r--src/Waylean.lean29
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