diff options
| author | Hannes Schulze <contact@haschu.me> | 2026-04-10 17:36:15 +0200 |
|---|---|---|
| committer | Hannes Schulze <contact@haschu.me> | 2026-04-10 17:36:15 +0200 |
| commit | dab858e92dfa5705d1aef7259e03b25747372d95 (patch) | |
| tree | a08fa2d015adda6a718b4abc5ece2648a6247735 /lib/Wayland/Display.lean | |
| parent | bfe6c4cee8b5afcd4078af319ab6b96f6695408b (diff) | |
implement registry wrapper
Diffstat (limited to 'lib/Wayland/Display.lean')
| -rw-r--r-- | lib/Wayland/Display.lean | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/lib/Wayland/Display.lean b/lib/Wayland/Display.lean index 63bd70d..704d7d4 100644 --- a/lib/Wayland/Display.lean +++ b/lib/Wayland/Display.lean @@ -21,7 +21,7 @@ section Interfaces /-- The name of an interface (e.g., `"wl_display"`), commonly used to resolve the corresponding interface description using the `Interface` class. -/ def InterfaceName : Type := String - deriving Repr, Nonempty, BEq, ToString + deriving Repr, Nonempty, BEq, ToString, Hashable /-- The numeric identifier of a request/event in an interface. -/ def OpCode : Type := UInt32 @@ -145,6 +145,7 @@ def DisplayM (σ : Type) : Type → Type := deriving instance Monad for DisplayM σ deriving instance MonadState σ for DisplayM σ +deriving instance MonadExcept IO.Error for DisplayM σ private instance : MonadLift (ReaderT (Display σ) (StateT σ IO)) (DisplayM σ) where monadLift := id |