@[specialize #[]]
def
Lean.HashSet.anyM
{α : Type u_1}
[inst : BEq α]
[inst : Hashable α]
{m : Type → Type}
[inst : 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.
@[inline]
def
Lean.HashSet.any
{α : Type u_1}
[inst : BEq α]
[inst : Hashable α]
(s : Lean.HashSet α)
(f : α → Bool)
:
O(n)
. Returns true
if f
returns true
for any element of the set.
Equations
- Lean.HashSet.any s f = Id.run (Lean.HashSet.anyM s f)
@[specialize #[]]
def
Lean.HashSet.allM
{α : Type u_1}
[inst : BEq α]
[inst : Hashable α]
{m : Type → Type}
[inst : 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.
@[inline]
def
Lean.HashSet.all
{α : Type u_1}
[inst : BEq α]
[inst : Hashable α]
(s : Lean.HashSet α)
(f : α → Bool)
:
O(n)
. Returns true
if f
returns true
for all elements of the set.
Equations
- Lean.HashSet.all s f = Id.run (Lean.HashSet.allM s f)
instance
Lean.HashSet.instBEqHashSet
{α : Type u_1}
[inst : BEq α]
[inst : Hashable α]
:
BEq (Lean.HashSet α)
Equations
- Lean.HashSet.instBEqHashSet = { beq := fun s t => (Lean.HashSet.all s fun x => Lean.HashSet.contains t x) && Lean.HashSet.all t fun x => Lean.HashSet.contains s x }
@[inline]
def
Lean.HashSet.insert'
{α : Type u_1}
[inst : BEq α]
[inst : Hashable α]
(s : Lean.HashSet α)
(a : α)
:
O(1)
amortized. Similar to insert
, but also returns a Boolean flag indicating whether an
existing entry has been replaced with a ↦ b↦ b
.
Equations
- Lean.HashSet.insert' s a = let oldSize := Lean.HashSet.size s; let s := Lean.HashSet.insert s a; (s, Lean.HashSet.size s == oldSize)
@[inline]
O(n)
. Obtain a HashSet
from an array.
Equations
- Lean.HashSet.ofArray as = Lean.HashSet.insertMany Lean.HashSet.empty as
@[inline]
O(n)
. Obtain a HashSet
from a list.
Equations
- Lean.HashSet.ofList as = Lean.HashSet.insertMany Lean.HashSet.empty as
@[inline]
def
Lean.HashSet.merge
{α : Type u}
[inst : BEq α]
[inst : Hashable α]
(s : Lean.HashSet α)
(t : Lean.HashSet α)
:
O(|t|)
amortized. Merge two HashSet
s.
Equations
- Lean.HashSet.merge s t = Lean.HashSet.fold (fun s a => Lean.HashSet.insert s a) s t