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

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

Instances For

• Aesop.UnionFind.instEmptyCollection
• Aesop.instInhabitedUnionFind

instance Aesop.instInhabitedUnionFind : {a : Type u_1} → {a_1 : BEq a} → {a_2 : Hashable a} → Inhabited (Aesop.UnionFind a)

Equations

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

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

Equations

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

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

Equations

• u.size = u.parents.size

def Aesop.UnionFind.add {α : Type u_1} [BEq α] [Hashable α] (x : α) (u : Aesop.UnionFind α) : Aesop.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 : Aesop.UnionFind α) : Aesop.UnionFind α

Equations

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

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

Equations

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

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

Equations

• Aesop.UnionFind.find? x u = match u.toRep.find? 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 : α) : Aesop.UnionFind α → Aesop.UnionFind α

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

Equations

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