Skip to content

Commit 6c3b16a

Browse files
authored
Remove diff function from TreeSet implementation
Removed the diff function for TreeSet instances.
1 parent 8ab1503 commit 6c3b16a

File tree

1 file changed

+0
-8
lines changed

1 file changed

+0
-8
lines changed

src/Std/Data/TreeSet/Basic.lean

Lines changed: 0 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -519,14 +519,6 @@ def inter (t₁ t₂ : TreeSet α cmp) : TreeSet α cmp :=
519519

520520
instance : Inter (TreeSet α cmp) := ⟨inter⟩
521521

522-
/--
523-
Computes the difference of the given tree sets.
524-
525-
This function always iterates through the smaller set.
526-
-/
527-
def diff (t₁ t₂ : TreeSet α cmp) : TreeSet α cmp :=
528-
⟨TreeMap.diff t₁.inner t₂.inner⟩
529-
530522
instance : SDiff (TreeSet α cmp) := ⟨diff⟩
531523

532524
/--

0 commit comments

Comments
 (0)