some initial cleanup

1 files changed, 7 insertions, 0 deletions

diff --git a/lib/Wayland/Basic/Lens.lean b/lib/Wayland/Basic/Lens.lean
index ee1e486..26455bb 100644
--- a/lib/Wayland/Basic/Lens.lean
+++ b/lib/Wayland/Basic/Lens.lean
@@ -1,3 +1,5 @@
+import Std.Data.HashMap
+
 /-!
 # Lenses
 
@@ -30,3 +32,8 @@ macro "mk_lens " field:ident : term => do
   `({ get := fun x => x.$field, set := fun i x => { x with $lval := i } })
 
 end Wayland
+
+/-- A lens into a hash-map, either containing .none or the value associated with the key. -/
+def Std.HashMap.lens {α β : Type} [BEq α] [Hashable α] (key : α) : Wayland.Lens (Std.HashMap α β) (Option β) where
+  get x := x.get? key
+  set v x := x.alter key fun _ ↦ v