From 92da08078a5459ca1089743eb58385e752bdb5fa Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Mon, 6 Apr 2026 07:19:48 +0200 Subject: fix generic new_ids --- lib/Wayland/Display.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'lib/Wayland/Display.lean') diff --git a/lib/Wayland/Display.lean b/lib/Wayland/Display.lean index 9ba60bc..70f5c67 100644 --- a/lib/Wayland/Display.lean +++ b/lib/Wayland/Display.lean @@ -101,7 +101,7 @@ class Interface (ι : InterfaceName) where version : UInt32 /-- Interface where all dependency interfaces can be resolvew. -/ -class ResolvedInterface (ι : InterfaceName) where +class ResolvedInterface (ι : InterfaceName) extends Interface ι where referencedInterfaces : Array ((ι' : InterfaceName) × Interface ι') contains_self : ∃ α, ⟨ι, α⟩ ∈ referencedInterfaces := by exists inferInstance; simp -- TODO: Verify that dependencies of interfaces are in referencedInterfaces @@ -367,8 +367,7 @@ private def DisplayM.ensureInterface (ι : InterfaceName) [iface : ResolvedInter events := iface'.events.map MessageDesc.toNative } (setComplete := if ι' == ι then 1 else 0) -/-- Get the `wl_display` instance within the display monad. -/ -def DisplayM.getDisplay : DisplayM σ (Object "wl_display") := do +def DisplayM.getDisplay' : DisplayM σ (Object "wl_display") := do let proxy ← Native.Proxy.fromDisplay (← read).disp return ⟨proxy⟩ -- cgit v1.3.1