From bda871da25c72248e6958b32a153c27e2b73f5cb Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Mon, 13 Jun 2022 11:12:30 +0200
Subject: [PATCH] feat: `RBTree.union/diff`

---
 src/Std/Data/RBTree.lean | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/src/Std/Data/RBTree.lean b/src/Std/Data/RBTree.lean
index 3d5ff8ca81..042668213e 100644
--- a/src/Std/Data/RBTree.lean
+++ b/src/Std/Data/RBTree.lean
@@ -101,6 +101,15 @@ def subset (t₁ t₂ : RBTree α cmp) : Bool :=
 def seteq (t₁ t₂ : RBTree α cmp) : Bool :=
   subset t₁ t₂ && subset t₂ t₁
 
+def union (t₁ t₂ : RBTree α cmp) : RBTree α cmp :=
+  if t₁.isEmpty then
+    t₂
+  else
+    t₂.fold .insert t₁
+
+def diff (t₁ t₂ : RBTree α cmp) : RBTree α cmp :=
+  t₂.fold .erase t₁
+
 end RBTree
 
 def rbtreeOf {α : Type u} (l : List α) (cmp : α → α → Ordering) : RBTree α cmp :=