lib/Wayland/Helpers.lean


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

import Wayland.Display
import Wayland.Protocols

-- Helpers that depend on the protocols and can thus not be included in `Display.lean`.

namespace Wayland

open Protocols

variable {σ : Type}

/-- Get the `wl_display` instance within the display monad. -/
def DisplayM.getDisplay : DisplayM σ WlDisplay := getDisplay'

end Wayland