Skip to content

Commit

Permalink
chore: add Union and SDiff instances for Std.RBSet (#775)
Browse files Browse the repository at this point in the history
  • Loading branch information
thelissimus authored May 6, 2024
1 parent 615a2a7 commit 789020b
Showing 1 changed file with 4 additions and 0 deletions.
4 changes: 4 additions & 0 deletions Std/Data/RBMap/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -822,6 +822,8 @@ If equal keys exist in both, the key from `t₂` is preferred.
def union (t₁ t₂ : RBSet α cmp) : RBSet α cmp :=
t₂.foldl .insert t₁

instance : Union (RBSet α cmp) := ⟨RBSet.union⟩

/--
`O(n₂ * log (n₁ + n₂))`. Merges the maps `t₁` and `t₂`. If equal keys exist in both,
then use `mergeFn a₁ a₂` to produce the new merged value.
Expand Down Expand Up @@ -857,6 +859,8 @@ def map (t : RBSet α cmpα) (f : α → β) : RBSet β cmpβ :=
-/
def sdiff (t₁ t₂ : RBSet α cmp) : RBSet α cmp := t₁.filter (!t₂.contains ·)

instance : SDiff (Std.RBSet α cmp) := ⟨RBSet.sdiff⟩

end RBSet

/- TODO(Leo): define dRBMap -/
Expand Down

0 comments on commit 789020b

Please sign in to comment.