From 37745b5174d334cc0d139177a9de377e950d647c Mon Sep 17 00:00:00 2001 From: "E.W.Ayers" Date: Thu, 1 Sep 2022 13:27:33 +0100 Subject: [PATCH] feat: intersectBy --- src/Lean/Data/RBMap.lean | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/Lean/Data/RBMap.lean b/src/Lean/Data/RBMap.lean index 0aefdd4793..cbec5f55be 100644 --- a/src/Lean/Data/RBMap.lean +++ b/src/Lean/Data/RBMap.lean @@ -386,6 +386,13 @@ def mergeBy (mergeFn : α → β → β → β) (t₁ t₂ : RBMap α β cmp) : | some b₁ => mergeFn a b₁ b₂ | none => b₂ +/-- Intersects the maps `t₁` and `t₂` using `mergeFn a b₁ b₂` to produce the new value. -/ +def intersectBy {γ : Type v₁} {δ : Type v₂} (mergeFn : α → β → γ → δ) (t₁ : RBMap α β cmp) (t₂ : RBMap α γ cmp) : RBMap α δ cmp := + t₁.fold (init := ∅) fun acc a b₁ => + match t₂.find? a with + | some b₂ => acc.insert a <| mergeFn a b₁ b₂ + | none => acc + end RBMap def rbmapOf {α : Type u} {β : Type v} (l : List (α × β)) (cmp : α → α → Ordering) : RBMap α β cmp :=