diff options
Diffstat (limited to 'src/Waylean.lean')
| -rw-r--r-- | src/Waylean.lean | 29 |
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 |
