instance
Lean.HashSet.instSingleton_batteries
{α : Type u_1}
[BEq α]
[Hashable α]
:
Singleton α (Lean.HashSet α)
Equations
- Lean.HashSet.instSingleton_batteries = { singleton := fun (x : α) => Lean.HashSet.empty.insert x }
instance
Lean.HashSet.instInsert_batteries
{α : Type u_1}
[BEq α]
[Hashable α]
:
Insert α (Lean.HashSet α)
Equations
- Lean.HashSet.instInsert_batteries = { insert := fun (a : α) (s : Lean.HashSet α) => s.insert a }
@[specialize #[]]
def
Lean.HashSet.anyM
{α : Type u_1}
[BEq α]
[Hashable α]
{m : Type → Type}
[Monad m]
(s : Lean.HashSet α)
(f : α → m Bool)
:
m Bool
O(n)
. Returns true
if f
returns true
for any element of the set.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[inline]
O(n)
. Returns true
if f
returns true
for any element of the set.
Equations
- s.any f = (s.anyM f).run
Instances For
@[specialize #[]]
def
Lean.HashSet.allM
{α : Type u_1}
[BEq α]
[Hashable α]
{m : Type → Type}
[Monad m]
(s : Lean.HashSet α)
(f : α → m Bool)
:
m Bool
O(n)
. Returns true
if f
returns true
for all elements of the set.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[inline]
O(n)
. Returns true
if f
returns true
for all elements of the set.
Equations
- s.all f = (s.allM f).run
Instances For
Equations
- Lean.HashSet.instBEq_batteries = { beq := fun (s t : Lean.HashSet α) => (s.all fun (x : α) => t.contains x) && t.all fun (x : α) => s.contains x }
@[inline]
O(1)
amortized. Similar to insert
, but also returns a Boolean flag indicating whether an
existing entry has been replaced with a => b
.
Instances For
@[inline]
O(n)
. Obtain a HashSet
from an array.
Equations
- Lean.HashSet.ofArray as = Lean.HashSet.empty.insertMany as
Instances For
@[inline]
O(n)
. Obtain a HashSet
from a list.
Equations
- Lean.HashSet.ofList as = Lean.HashSet.empty.insertMany as