Std.Data.PersistentHashSet

source

structure Std.PersistentHashSet (α : Type u) [inst : BEq α] [inst : Hashable α] :

Type u

set : Std.PersistentHashMap α Unit

source

@[inline]

abbrev Std.PHashSet (α : Type u) [inst : BEq α] [inst : Hashable α] :

Type u

Equations

Std.PHashSet α = Std.PersistentHashSet α

source

@[inline]

def Std.PersistentHashSet.empty {α : Type u_1} [inst : BEq α] [inst : Hashable α] :

Std.PersistentHashSet α

Equations

Std.PersistentHashSet.empty = { set := Std.PersistentHashMap.empty }

source

instance Std.PersistentHashSet.instInhabitedPersistentHashSet {α : Type u_1} [inst : BEq α] [inst : Hashable α] :

Inhabited (Std.PersistentHashSet α)

Equations

Std.PersistentHashSet.instInhabitedPersistentHashSet = { default := Std.PersistentHashSet.empty }

source

instance Std.PersistentHashSet.instEmptyCollectionPersistentHashSet {α : Type u_1} [inst : BEq α] [inst : Hashable α] :

EmptyCollection (Std.PersistentHashSet α)

Equations

Std.PersistentHashSet.instEmptyCollectionPersistentHashSet = { emptyCollection := Std.PersistentHashSet.empty }

source

@[inline]

def Std.PersistentHashSet.isEmpty {α : Type u_1} :

{x : BEq α} → {x_1 : Hashable α} → Std.PersistentHashSet α → Bool

Equations

Std.PersistentHashSet.isEmpty s = Std.PersistentHashMap.isEmpty s.set

source

@[inline]

def Std.PersistentHashSet.insert {α : Type u_1} :

{x : BEq α} → {x_1 : Hashable α} → Std.PersistentHashSet α → α → Std.PersistentHashSet α

Equations

Std.PersistentHashSet.insert s a = { set := Std.PersistentHashMap.insert s.set a () }

source

@[inline]

def Std.PersistentHashSet.erase {α : Type u_1} :

{x : BEq α} → {x_1 : Hashable α} → Std.PersistentHashSet α → α → Std.PersistentHashSet α

Equations

Std.PersistentHashSet.erase s a = { set := Std.PersistentHashMap.erase s.set a }

source

@[inline]

def Std.PersistentHashSet.find? {α : Type u_1} :

{x : BEq α} → {x_1 : Hashable α} → Std.PersistentHashSet α → α → Option α

Equations

Std.PersistentHashSet.find? s a = match Std.PersistentHashMap.findEntry? s.set a with | some (a, x) => some a | none => none

source

@[inline]

def Std.PersistentHashSet.contains {α : Type u_1} :

{x : BEq α} → {x_1 : Hashable α} → Std.PersistentHashSet α → α → Bool

Equations

Std.PersistentHashSet.contains s a = Std.PersistentHashMap.contains s.set a

source

@[inline]

def Std.PersistentHashSet.size {α : Type u_1} :

{x : BEq α} → {x_1 : Hashable α} → Std.PersistentHashSet α → Nat

Equations

Std.PersistentHashSet.size s = s.set.size

source

@[inline]

def Std.PersistentHashSet.foldM {α : Type u_1} :

{x : BEq α} → {x_1 : Hashable α} → {β : Type v} → {m : Type v → Type v} → [inst : Monad m] → (β → α → m β) → β → Std.PersistentHashSet α → m β

Equations

Std.PersistentHashSet.foldM f init s = Std.PersistentHashMap.foldlM s.set (fun d a x => f d a) init

source

@[inline]

def Std.PersistentHashSet.fold {α : Type u_1} :

{x : BEq α} → {x_1 : Hashable α} → {β : Type v} → (β → α → β) → β → Std.PersistentHashSet α → β

Equations

Std.PersistentHashSet.fold f init s = Id.run (Std.PersistentHashSet.foldM f init s)