From 37d2f5a8d4e1623d1685ee1d545d2e0e31128352 Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Sat, 6 Jun 2026 00:10:15 +0200 Subject: some initial cleanup --- lib/Wayland/Basic/Lens.lean | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'lib') 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 -- cgit v1.3.1