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

A hash set that preserves the order of insertions.

• toArray : Array α
• toHashSet : Std.HashSet α

def Aesop.instInhabitedOrderedHashSet.default {a✝ : Type u_1} {a✝¹ : BEq a✝} {a✝² : Hashable a✝} : OrderedHashSet a✝

Equations

• Aesop.instInhabitedOrderedHashSet.default = { toArray := default, toHashSet := default }

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

Equations

• Aesop.instInhabitedOrderedHashSet = { default := Aesop.instInhabitedOrderedHashSet.default }

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

Equations

• Aesop.OrderedHashSet.instEmptyCollection = { emptyCollection := { toArray := #[], toHashSet := ∅ } }

def Aesop.OrderedHashSet.emptyWithCapacity {α : Type u_1} [BEq α] [Hashable α] (n : Nat) : OrderedHashSet α

Equations

• Aesop.OrderedHashSet.emptyWithCapacity n = { toArray := Array.emptyWithCapacity n, toHashSet := Std.HashSet.emptyWithCapacity n }

def Aesop.OrderedHashSet.insert {α : Type u_1} [BEq α] [Hashable α] (x : α) (s : OrderedHashSet α) : OrderedHashSet α

Equations

• Aesop.OrderedHashSet.insert x s = if x ∈ s.toHashSet then s else { toArray := s.toArray.push x, toHashSet := s.toHashSet.insert x }

def Aesop.OrderedHashSet.insertMany {α : Type u_1} [BEq α] [Hashable α] {ρ : Type u_2} [ForIn Id ρ α] (xs : ρ) (s : OrderedHashSet α) : OrderedHashSet α

Equations

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

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

Equations

• Aesop.OrderedHashSet.ofArray xs = Aesop.OrderedHashSet.insertMany xs ∅

def Aesop.OrderedHashSet.contains {α : Type u_1} [BEq α] [Hashable α] (x : α) (s : OrderedHashSet α) : Bool

Equations

• Aesop.OrderedHashSet.contains x s = s.toHashSet.contains x

instance Aesop.OrderedHashSet.instMembership {α : Type u_1} [BEq α] [Hashable α] : Membership α (OrderedHashSet α)

Equations

• Aesop.OrderedHashSet.instMembership = { mem := fun (s : Aesop.OrderedHashSet α) (x : α) => x ∈ s.toHashSet }

instance Aesop.OrderedHashSet.instDecidableMem {α : Type u_1} [BEq α] [Hashable α] {x : α} {s : OrderedHashSet α} : Decidable (x ∈ s)

Equations

• Aesop.OrderedHashSet.instDecidableMem = inferInstanceAs (Decidable (x ∈ s.toHashSet))

@[specialize #[]]

def Aesop.OrderedHashSet.foldlM {α : Type u_1} [BEq α] [Hashable α] {m : Type u_2 → Type u_3} {β : Type u_2} [Monad m] (f : β → α → m β) (init : β) (s : OrderedHashSet α) : m β

Equations

• Aesop.OrderedHashSet.foldlM f init s = Array.foldlM f init s.toArray

def Aesop.OrderedHashSet.foldl {α : Type u_1} [BEq α] [Hashable α] {β : Type u_2} (f : β → α → β) (init : β) (s : OrderedHashSet α) : β

Equations

• Aesop.OrderedHashSet.foldl f init s = Array.foldl f init s.toArray

@[specialize #[]]

def Aesop.OrderedHashSet.foldrM {α : Type u_1} [BEq α] [Hashable α] {m : Type u_2 → Type u_3} {β : Type u_2} [Monad m] (f : α → β → m β) (init : β) (s : OrderedHashSet α) : m β

Equations

• Aesop.OrderedHashSet.foldrM f init s = Array.foldrM f init s.toArray

def Aesop.OrderedHashSet.foldr {α : Type u_1} [BEq α] [Hashable α] {β : Type u_2} (f : α → β → β) (init : β) (s : OrderedHashSet α) : β

Equations

• Aesop.OrderedHashSet.foldr f init s = Array.foldr f init s.toArray

instance Aesop.OrderedHashSet.instForIn {α : Type u_1} [BEq α] [Hashable α] {m : Type u_2 → Type u_3} : ForIn m (OrderedHashSet α) α

Equations

• Aesop.OrderedHashSet.instForIn = { forIn := fun {β : Type ?u.30} [Monad m] (s : Aesop.OrderedHashSet α) (b : β) (f : α → β → m (ForInStep β)) => forIn s.toArray b f }