instance
Lake.OrdHashSet.instCoeOrdHashSetHashSet
{α : Type u_1}
[Hashable α]
[BEq α]
:
Coe (Lake.OrdHashSet α) (Lean.HashSet α)
Instances For
Instances For
def
Lake.OrdHashSet.appendArray
{α : Type u_1}
[Hashable α]
[BEq α]
(self : Lake.OrdHashSet α)
(arr : Array α)
:
Instances For
instance
Lake.OrdHashSet.instHAppendOrdHashSetArray
{α : Type u_1}
[Hashable α]
[BEq α]
:
HAppend (Lake.OrdHashSet α) (Array α) (Lake.OrdHashSet α)
def
Lake.OrdHashSet.append
{α : Type u_1}
[Hashable α]
[BEq α]
(self : Lake.OrdHashSet α)
(other : Lake.OrdHashSet α)
:
Instances For
Instances For
@[inline]
def
Lake.OrdHashSet.all
{α : Type u_1}
[Hashable α]
[BEq α]
(f : α → Bool)
(self : Lake.OrdHashSet α)
:
Instances For
@[inline]
def
Lake.OrdHashSet.any
{α : Type u_1}
[Hashable α]
[BEq α]
(f : α → Bool)
(self : Lake.OrdHashSet α)
:
Instances For
@[inline]
def
Lake.OrdHashSet.foldl
{α : Type u_1}
[Hashable α]
[BEq α]
{β : Type u_2}
(f : β → α → β)
(init : β)
(self : Lake.OrdHashSet α)
:
β
Instances For
@[inline]
def
Lake.OrdHashSet.foldlM
{α : Type u_1}
[Hashable α]
[BEq α]
{m : Type u_2 → Type u_3}
{β : Type u_2}
[Monad m]
(f : β → α → m β)
(init : β)
(self : Lake.OrdHashSet α)
:
m β
Instances For
@[inline]
def
Lake.OrdHashSet.foldr
{α : Type u_1}
[Hashable α]
[BEq α]
{β : Type u_2}
(f : α → β → β)
(init : β)
(self : Lake.OrdHashSet α)
:
β
Instances For
@[inline]
def
Lake.OrdHashSet.foldrM
{α : Type u_1}
[Hashable α]
[BEq α]
{m : Type u_2 → Type u_3}
{β : Type u_2}
[Monad m]
(f : α → β → m β)
(init : β)
(self : Lake.OrdHashSet α)
:
m β
Instances For
instance
Lake.OrdHashSet.instForInOrdHashSet
{α : Type u_1}
[Hashable α]
[BEq α]
{m : Type u_2 → Type u_3}
:
ForIn m (Lake.OrdHashSet α) α