lib/Wayland/Native.lean


1
2
3
4
5
6
7
8
9

private opaque DisplayP : NonemptyType
def Display : Type := DisplayP.type
instance : Nonempty Display := DisplayP.property

@[extern "waylean_display_new"]
opaque Display.new : (name : @& Option String) → IO Display

@[extern "waylean_display_get_version"]
opaque Display.getVersion : (display : @& Display) → IO UInt32