- set : Lean.PersistentHashMap α Unit
Instances For
@[inline, reducible]
Equations
Instances For
@[inline]
Equations
- Lean.PersistentHashSet.empty = { set := Lean.PersistentHashMap.empty }
Instances For
instance
Lean.PersistentHashSet.instInhabitedPersistentHashSet
{α : Type u_1}
[BEq α]
[Hashable α]
:
Equations
- Lean.PersistentHashSet.instInhabitedPersistentHashSet = { default := Lean.PersistentHashSet.empty }
instance
Lean.PersistentHashSet.instEmptyCollectionPersistentHashSet
{α : Type u_1}
[BEq α]
[Hashable α]
:
Equations
- Lean.PersistentHashSet.instEmptyCollectionPersistentHashSet = { emptyCollection := Lean.PersistentHashSet.empty }
@[inline]
def
Lean.PersistentHashSet.isEmpty
{α : Type u_1}
:
{x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashSet α → Bool
Equations
Instances For
@[inline]
def
Lean.PersistentHashSet.insert
{α : Type u_1}
:
{x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashSet α → α → Lean.PersistentHashSet α
Equations
- Lean.PersistentHashSet.insert s a = { set := Lean.PersistentHashMap.insert s.set a () }
Instances For
@[inline]
def
Lean.PersistentHashSet.erase
{α : Type u_1}
:
{x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashSet α → α → Lean.PersistentHashSet α
Equations
- Lean.PersistentHashSet.erase s a = { set := Lean.PersistentHashMap.erase s.set a }
Instances For
@[inline]
def
Lean.PersistentHashSet.find?
{α : Type u_1}
:
{x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashSet α → α → Option α
Equations
- Lean.PersistentHashSet.find? s a = match Lean.PersistentHashMap.findEntry? s.set a with | some (a, snd) => some a | none => none
Instances For
@[inline]
def
Lean.PersistentHashSet.contains
{α : Type u_1}
:
{x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashSet α → α → Bool
Equations
Instances For
@[inline]
def
Lean.PersistentHashSet.size
{α : Type u_1}
:
{x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashSet α → Nat
Equations
- Lean.PersistentHashSet.size s = s.set.size
Instances For
@[inline]
Equations
- Lean.PersistentHashSet.foldM f init s = Lean.PersistentHashMap.foldlM s.set (fun d a x => f d a) init
Instances For
@[inline]
def
Lean.PersistentHashSet.fold
{α : Type u_1}
:
{x : BEq α} → {x_1 : Hashable α} → {β : Type v} → (β → α → β) → β → Lean.PersistentHashSet α → β
Equations
- Lean.PersistentHashSet.fold f init s = Id.run (Lean.PersistentHashSet.foldM f init s)