- set : PersistentHashMap α Unit
Instances For
@[inline]
Equations
Instances For
Equations
Equations
@[inline]
def
Lean.PersistentHashSet.isEmpty
{α : Type u_1}
{x✝ : BEq α}
{x✝¹ : Hashable α}
(s : PersistentHashSet α)
:
Equations
Instances For
@[inline]
def
Lean.PersistentHashSet.insert
{α : Type u_1}
{x✝ : BEq α}
{x✝¹ : Hashable α}
(s : PersistentHashSet α)
(a : α)
:
Equations
Instances For
@[inline]
def
Lean.PersistentHashSet.erase
{α : Type u_1}
{x✝ : BEq α}
{x✝¹ : Hashable α}
(s : PersistentHashSet α)
(a : α)
:
Equations
Instances For
@[inline]
def
Lean.PersistentHashSet.find?
{α : Type u_1}
{x✝ : BEq α}
{x✝¹ : Hashable α}
(s : PersistentHashSet α)
(a : α)
:
Option α
Equations
Instances For
@[inline]
def
Lean.PersistentHashSet.contains
{α : Type u_1}
{x✝ : BEq α}
{x✝¹ : Hashable α}
(s : PersistentHashSet α)
(a : α)
:
Equations
Instances For
@[inline]
def
Lean.PersistentHashSet.foldM
{α : Type u_1}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : Type v → Type v}
[Monad m]
(f : β → α → m β)
(init : β)
(s : PersistentHashSet α)
:
m β
Equations
Instances For
@[inline]
def
Lean.PersistentHashSet.fold
{α : Type u_1}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
(f : β → α → β)
(init : β)
(s : PersistentHashSet α)
:
β
Equations
Instances For
def
Lean.PersistentHashSet.toList
{α : Type u_1}
{x✝ : BEq α}
{x✝¹ : Hashable α}
(s : PersistentHashSet α)
:
List α
Equations
Instances For
instance
Lean.PersistentHashSet.instForIn
{α : Type u_1}
{m : Type u_2 → Type u_3}
{x✝ : BEq α}
{x✝¹ : Hashable α}
:
ForIn m (PersistentHashSet α) α