def Auto.mergeHashSet {α : Type u} [BEq α] [Hashable α] (a1 a2 : Std.HashSet α) : Std.HashSet α

Equations

• Auto.mergeHashSet a1 a2 = if a1.size < a2.size then a2.insertMany a1.toArray else a1.insertMany a2.toArray

def Auto.mergeArray {α : Type u_1} (a1 a2 : Array α) : Array α

Equations

• Auto.mergeArray a1 a2 = if a1.size < a2.size then a2 ++ a1 else a1 ++ a2

def Auto.tallyArrayHashable {α : Type u_1} [Hashable α] [BEq α] (xs : Array α) : Array (α × Nat)

Equations

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

class Auto.Container {α : Type u} (C : Type v → Type w) : Type (max (max u (v + 1)) w)

Effectively a map from α to arbitrary type

• get? {β : Type v} : C β → α → Option β
• insert {β : Type v} : C β → α → β → C β
• insertCorrect₁ {β : Type v} {val : β} (c : C β) (k : α) (v : β) : get? (insert c k v) k = some val
• insertCorrect₂ {β : Type v} (c : C β) (k₁ k₂ : α) (v : β) : k₁ ≠ k₂ → get? (insert c k₁ v) k₂ = get? c k₂