From 2c39ecdbff16026daa2fd357ad520e412adb620c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 26 Jun 2019 06:30:24 -0700
Subject: [PATCH] chore(library/init/lean/disjoint_set): remove dead code

---
 library/init/lean/disjoint_set.lean | 53 -----------------------------
 1 file changed, 53 deletions(-)
 delete mode 100644 library/init/lean/disjoint_set.lean

diff --git a/library/init/lean/disjoint_set.lean b/library/init/lean/disjoint_set.lean
deleted file mode 100644
index a544919b63..0000000000
--- a/library/init/lean/disjoint_set.lean
+++ /dev/null
@@ -1,53 +0,0 @@
-/-
-Copyright (c) 2018 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Author: Leonardo de Moura
--/
-prelude
-import init.data.hashmap.basic
-
-/- Disjoint set datastructure using union-find algorithm.
-   We use hashmaps to implement. Thus, we should be disjoint sets
-   linearly for optimal performace. -/
-
-namespace Lean
-universes u
-structure DisjointSet.Node (α : Type u) :=
-(find : α)
-(rank : Nat := 0)
-
-structure DisjointSet (α : Type u) [HasBeq α] [Hashable α] : Type u :=
-(map : HashMap α (DisjointSet.Node α))
-
-def mkDisjointSet (α : Type u) [HasBeq α] [Hashable α] : DisjointSet α :=
-⟨mkHashMap⟩
-
-variables {α : Type u}
-
-namespace DisjointSet
-variables [DecidableEq α] [Hashable α]
-
-private def findAux : Nat → α → HashMap α (Node α) → Node α
-| 0     a m := { find := a, rank := 0 }
-| (n+1) a m :=
-  match m.find a with
-  | some r := if r.find = a then r else findAux n r.find m
-  | none   := { find := a, rank := 0 }
-
-def find : DisjointSet α → α → α
-| ⟨m⟩ a := (findAux m.size a m).find
-
-def rank : DisjointSet α → α → Nat
-| ⟨m⟩ a := (findAux m.size a m).rank
-
-def merge : DisjointSet α → α → α → DisjointSet α
-| ⟨m⟩ a b :=
-  let ra := findAux m.size a m in
-  let rb := findAux m.size b m in
-  if ra.find = rb.find then ⟨m⟩
-  else if ra.rank < rb.rank then ⟨m.insert a { find := b }⟩
-  else if ra.rank = rb.rank then ⟨(m.insert a { find := b }).insert b { find := b, rank := rb.rank + 1 }⟩
-  else ⟨m.insert b { find := a }⟩
-
-end DisjointSet
-end Lean