diff options
Diffstat (limited to 'lib/Wayland/Basic')
| -rw-r--r-- | lib/Wayland/Basic/Lens.lean | 7 |
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 |