structure Aesop.UnionFind (α : Type u_1) [BEq α] [Hashable α] : Type u_1

• parents : Array USize
• sizes : Array USize
• toRep : Std.HashMap α USize

instance Aesop.instInhabitedUnionFind {a✝ : Type u_1} {a✝¹ : BEq a✝} {a✝² : Hashable a✝} : Inhabited (UnionFind a✝)

Equations

• Aesop.instInhabitedUnionFind = { default := { parents := default, sizes := default, toRep := default } }

instance Aesop.UnionFind.instEmptyCollection {α : Type u_1} [BEq α] [Hashable α] : EmptyCollection (UnionFind α)

Equations

• Aesop.UnionFind.instEmptyCollection = { emptyCollection := { parents := #[], sizes := #[], toRep := ∅ } }

def Aesop.UnionFind.size {α : Type u_1} [BEq α] [Hashable α] (u : UnionFind α) : Nat

Equations

• u.size = u.parents.size

def Aesop.UnionFind.add {α : Type u_1} [BEq α] [Hashable α] (x : α) (u : UnionFind α) : UnionFind α

Equations

• One or more equations did not get rendered due to their size.

def Aesop.UnionFind.addArray {α : Type u_1} [BEq α] [Hashable α] (xs : Array α) (u : UnionFind α) : UnionFind α

Equations

• Aesop.UnionFind.addArray xs u = Array.foldl (fun (u : Aesop.UnionFind α) (x : α) => Aesop.UnionFind.add x u) u xs

def Aesop.UnionFind.ofArray {α : Type u_1} [BEq α] [Hashable α] (xs : Array α) : UnionFind α

Equations

• Aesop.UnionFind.ofArray xs = Aesop.UnionFind.addArray xs ∅

def Aesop.UnionFind.find? {α : Type u_1} [BEq α] [Hashable α] (x : α) (u : UnionFind α) : Option USize × UnionFind α

Equations

• Aesop.UnionFind.find? x u = match u.toRep[x]? with | none => (none, u) | some rep => match Aesop.UnionFind.findRep✝ rep u with | (rep, u) => (some rep, u)

@[implemented_by _private.Aesop.Util.UnionFind.0.Aesop.UnionFind.mergeUnsafe]

opaque Aesop.UnionFind.merge {α : Type u_1} [BEq α] [Hashable α] (x y : α) : UnionFind α → UnionFind α

def Aesop.UnionFind.sets {α : Type v} [BEq α] [Hashable α] (u : UnionFind α) : Array (Array α) × UnionFind α

Equations

• One or more equations did not get rendered due to their size.

def Aesop.cluster {α : Type (max u_1 u_2)} {β : Type u_2} [BEq α] [Hashable α] [BEq β] [Hashable β] (f : α → Array β) (as : Array α) : Array (Array α)

Cluster the as according to which bs are associated to them by f. Two members a₁, a₂ of as are put in the same cluster iff f a₁ ∩ f a₂ ≠ ∅.

Equations

• One or more equations did not get rendered due to their size.