feat: deprecated find, fold, foldM, mergeBy functions for the tree map (#7036)
This PR adds some deprecated function aliases to the tree map in order to ease the transition from the `RBMap` to the tree map. --------- Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
This commit is contained in:
Paul Reichert
GitHub
parent
04fe72fee0
commit
6ac530aa1a
6 changed files with 148 additions and 1 deletions
|
|
@ -179,6 +179,10 @@ Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
|
|||
def get? [LawfulEqCmp cmp] (t : DTreeMap α β cmp) (a : α) : Option (β a) :=
|
||||
letI : Ord α := ⟨cmp⟩; t.inner.get? a
|
||||
|
||||
@[inline, inherit_doc get?, deprecated get? (since := "2025-02-12")]
|
||||
def find? [LawfulEqCmp cmp] (t : DTreeMap α β cmp) (a : α) : Option (β a) :=
|
||||
t.get? a
|
||||
|
||||
/--
|
||||
Given a proof that a mapping for the given key is present, retrieves the mapping for the given key.
|
||||
|
||||
|
|
@ -197,6 +201,10 @@ Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
|
|||
def get! [LawfulEqCmp cmp] (t : DTreeMap α β cmp) (a : α) [Inhabited (β a)] : β a :=
|
||||
letI : Ord α := ⟨cmp⟩; t.inner.get! a
|
||||
|
||||
@[inline, inherit_doc get!, deprecated get! (since := "2025-02-12")]
|
||||
def find! [LawfulEqCmp cmp] (t : DTreeMap α β cmp) (a : α) [Inhabited (β a)] : β a :=
|
||||
t.get! a
|
||||
|
||||
/--
|
||||
Tries to retrieve the mapping for the given key, returning `fallback` if no such mapping is present.
|
||||
|
||||
|
|
@ -206,6 +214,10 @@ Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
|
|||
def getD [LawfulEqCmp cmp] (t : DTreeMap α β cmp) (a : α) (fallback : β a) : β a :=
|
||||
letI : Ord α := ⟨cmp⟩; t.inner.getD a fallback
|
||||
|
||||
@[inline, inherit_doc getD, deprecated getD (since := "2025-02-12")]
|
||||
def findD [LawfulEqCmp cmp] (t : DTreeMap α β cmp) (a : α) (fallback : β a) : β a :=
|
||||
t.getD a fallback
|
||||
|
||||
namespace Const
|
||||
open Internal (Impl)
|
||||
|
||||
|
|
@ -218,6 +230,10 @@ Tries to retrieve the mapping for the given key, returning `none` if no such map
|
|||
def get? (t : DTreeMap α β cmp) (a : α) : Option β :=
|
||||
letI : Ord α := ⟨cmp⟩; Impl.Const.get? a t.inner
|
||||
|
||||
@[inline, inherit_doc get?, deprecated get? (since := "2025-02-12")]
|
||||
def find? (t : DTreeMap α β cmp) (a : α) : Option β :=
|
||||
get? t a
|
||||
|
||||
/--
|
||||
Given a proof that a mapping for the given key is present, retrieves the mapping for the given key.
|
||||
-/
|
||||
|
|
@ -232,6 +248,10 @@ Tries to retrieve the mapping for the given key, panicking if no such mapping is
|
|||
def get! (t : DTreeMap α β cmp) (a : α) [Inhabited β] : β :=
|
||||
letI : Ord α := ⟨cmp⟩; Impl.Const.get! a t.inner
|
||||
|
||||
@[inline, inherit_doc get!, deprecated get! (since := "2025-02-12")]
|
||||
def find! (t : DTreeMap α β cmp) (a : α) [Inhabited β] : β :=
|
||||
get! t a
|
||||
|
||||
/--
|
||||
Tries to retrieve the mapping for the given key, returning `fallback` if no such mapping is present.
|
||||
-/
|
||||
|
|
@ -239,6 +259,10 @@ Tries to retrieve the mapping for the given key, returning `fallback` if no such
|
|||
def getD (t : DTreeMap α β cmp) (a : α) (fallback : β) : β :=
|
||||
letI : Ord α := ⟨cmp⟩; Impl.Const.getD a t.inner fallback
|
||||
|
||||
@[inline, inherit_doc getD, deprecated getD (since := "2025-02-12")]
|
||||
def findD (t : DTreeMap α β cmp) (a : α) (fallback : β) : β :=
|
||||
getD t a fallback
|
||||
|
||||
end Const
|
||||
|
||||
variable {δ : Type w} {m : Type w → Type w₂} [Monad m]
|
||||
|
|
@ -255,6 +279,10 @@ Folds the given monadic function over the mappings in the map in ascending order
|
|||
def foldlM (f : δ → (a : α) → β a → m δ) (init : δ) (t : DTreeMap α β cmp) : m δ :=
|
||||
t.inner.foldlM f init
|
||||
|
||||
@[inline, inherit_doc foldlM, deprecated foldlM (since := "2025-02-12")]
|
||||
def foldM (f : δ → (a : α) → β a → m δ) (init : δ) (t : DTreeMap α β cmp) : m δ :=
|
||||
t.foldlM f init
|
||||
|
||||
/--
|
||||
Folds the given function over the mappings in the map in ascending order.
|
||||
-/
|
||||
|
|
@ -262,6 +290,10 @@ Folds the given function over the mappings in the map in ascending order.
|
|||
def foldl (f : δ → (a : α) → β a → δ) (init : δ) (t : DTreeMap α β cmp) : δ :=
|
||||
t.inner.foldl f init
|
||||
|
||||
@[inline, inherit_doc foldl, deprecated foldl (since := "2025-02-12")]
|
||||
def fold (f : δ → (a : α) → β a → δ) (init : δ) (t : DTreeMap α β cmp) : δ :=
|
||||
t.foldl f init
|
||||
|
||||
/-- Carries out a monadic action on each mapping in the tree map in ascending order. -/
|
||||
@[inline]
|
||||
def forM (f : (a : α) → β a → m PUnit) (t : DTreeMap α β cmp) : m PUnit :=
|
||||
|
|
@ -332,6 +364,11 @@ def mergeWith [LawfulEqCmp cmp] (mergeFn : (a : α) → β a → β a → β a)
|
|||
DTreeMap α β cmp :=
|
||||
letI : Ord α := ⟨cmp⟩; ⟨t₁.inner.mergeWith mergeFn t₂.inner t₁.wf.balanced |>.impl, t₁.wf.mergeWith⟩
|
||||
|
||||
@[inline, inherit_doc mergeWith, deprecated mergeWith (since := "2025-02-12")]
|
||||
def mergeBy [LawfulEqCmp cmp] (mergeFn : (a : α) → β a → β a → β a) (t₁ t₂ : DTreeMap α β cmp) :
|
||||
DTreeMap α β cmp :=
|
||||
mergeWith mergeFn t₁ t₂
|
||||
|
||||
namespace Const
|
||||
|
||||
variable {β : Type v}
|
||||
|
|
@ -349,6 +386,10 @@ def mergeWith (mergeFn : α → β → β → β) (t₁ t₂ : DTreeMap α β cm
|
|||
letI : Ord α := ⟨cmp⟩;
|
||||
⟨Impl.Const.mergeWith mergeFn t₁.inner t₂.inner t₁.wf.balanced |>.impl, t₁.wf.constMergeBy⟩
|
||||
|
||||
@[inline, inherit_doc mergeWith, deprecated mergeWith (since := "2025-02-12")]
|
||||
def mergeBy (mergeFn : α → β → β → β) (t₁ t₂ : DTreeMap α β cmp) : DTreeMap α β cmp :=
|
||||
mergeWith mergeFn t₁ t₂
|
||||
|
||||
end Const
|
||||
|
||||
/--
|
||||
|
|
|
|||
|
|
@ -150,6 +150,10 @@ def erase (t : Raw α β cmp) (a : α) : Raw α β cmp :=
|
|||
def get? [LawfulEqCmp cmp] (t : Raw α β cmp) (a : α) : Option (β a) :=
|
||||
letI : Ord α := ⟨cmp⟩; t.inner.get? a
|
||||
|
||||
@[inline, inherit_doc get?, deprecated get? (since := "2025-02-12")]
|
||||
def find? [LawfulEqCmp cmp] (t : Raw α β cmp) (a : α) : Option (β a) :=
|
||||
t.get? a
|
||||
|
||||
@[inline, inherit_doc DTreeMap.get]
|
||||
def get [LawfulEqCmp cmp] (t : Raw α β cmp) (a : α) (h : a ∈ t) : β a :=
|
||||
letI : Ord α := ⟨cmp⟩; t.inner.get a h
|
||||
|
|
@ -158,18 +162,31 @@ def get [LawfulEqCmp cmp] (t : Raw α β cmp) (a : α) (h : a ∈ t) : β a :=
|
|||
def get! [LawfulEqCmp cmp] (t : Raw α β cmp) (a : α) [Inhabited (β a)] : β a :=
|
||||
letI : Ord α := ⟨cmp⟩; t.inner.get! a
|
||||
|
||||
@[inline, inherit_doc get!, deprecated get! (since := "2025-02-12")]
|
||||
def find! [LawfulEqCmp cmp] (t : Raw α β cmp) (a : α) [Inhabited (β a)] : β a :=
|
||||
t.get! a
|
||||
|
||||
@[inline, inherit_doc DTreeMap.getD]
|
||||
def getD [LawfulEqCmp cmp] (t : Raw α β cmp) (a : α) (fallback : β a) : β a :=
|
||||
letI : Ord α := ⟨cmp⟩; t.inner.getD a fallback
|
||||
|
||||
@[inline, inherit_doc getD, deprecated getD (since := "2025-02-12")]
|
||||
def findD [LawfulEqCmp cmp] (t : Raw α β cmp) (a : α) (fallback : β a) : β a :=
|
||||
t.getD a fallback
|
||||
|
||||
namespace Const
|
||||
open Internal (Impl)
|
||||
|
||||
variable {β : Type v}
|
||||
|
||||
@[inline, inherit_doc DTreeMap.get?] def get? (t : Raw α β cmp) (a : α) : Option β :=
|
||||
@[inline, inherit_doc DTreeMap.get?]
|
||||
def get? (t : Raw α β cmp) (a : α) : Option β :=
|
||||
letI : Ord α := ⟨cmp⟩; Impl.Const.get? a t.inner
|
||||
|
||||
@[inline, inherit_doc get?, deprecated get? (since := "2025-02-12")]
|
||||
def find? (t : Raw α β cmp) (a : α) : Option β :=
|
||||
get? t a
|
||||
|
||||
@[inline, inherit_doc DTreeMap.get]
|
||||
def get (t : Raw α β cmp) (a : α) (h : a ∈ t) : β :=
|
||||
letI : Ord α := ⟨cmp⟩; Impl.Const.get a t.inner h
|
||||
|
|
@ -178,10 +195,18 @@ def get (t : Raw α β cmp) (a : α) (h : a ∈ t) : β :=
|
|||
def get! (t : Raw α β cmp) (a : α) [Inhabited β] : β :=
|
||||
letI : Ord α := ⟨cmp⟩; Impl.Const.get! a t.inner
|
||||
|
||||
@[inline, inherit_doc get!, deprecated get! (since := "2025-02-12")]
|
||||
def find! (t : Raw α β cmp) (a : α) [Inhabited β] : β :=
|
||||
get! t a
|
||||
|
||||
@[inline, inherit_doc DTreeMap.getD]
|
||||
def getD (t : Raw α β cmp) (a : α) (fallback : β) : β :=
|
||||
letI : Ord α := ⟨cmp⟩; Impl.Const.getD a t.inner fallback
|
||||
|
||||
@[inline, inherit_doc getD, deprecated getD (since := "2025-02-12")]
|
||||
def findD (t : Raw α β cmp) (a : α) (fallback : β) : β :=
|
||||
getD t a fallback
|
||||
|
||||
end Const
|
||||
|
||||
variable {δ : Type w} {m : Type w → Type w₂} [Monad m]
|
||||
|
|
@ -194,10 +219,18 @@ def filter (f : (a : α) → β a → Bool) (t : Raw α β cmp) : Raw α β cmp
|
|||
def foldlM (f : δ → (a : α) → β a → m δ) (init : δ) (t : Raw α β cmp) : m δ :=
|
||||
t.inner.foldlM f init
|
||||
|
||||
@[inline, inherit_doc foldlM, deprecated foldlM (since := "2025-02-12")]
|
||||
def foldM (f : δ → (a : α) → β a → m δ) (init : δ) (t : Raw α β cmp) : m δ :=
|
||||
t.foldlM f init
|
||||
|
||||
@[inline, inherit_doc DTreeMap.foldl]
|
||||
def foldl (f : δ → (a : α) → β a → δ) (init : δ) (t : Raw α β cmp) : δ :=
|
||||
t.inner.foldl f init
|
||||
|
||||
@[inline, inherit_doc foldl, deprecated foldl (since := "2025-02-12")]
|
||||
def fold (f : δ → (a : α) → β a → δ) (init : δ) (t : Raw α β cmp) : δ :=
|
||||
t.foldl f init
|
||||
|
||||
@[inline, inherit_doc DTreeMap.forM]
|
||||
def forM (f : (a : α) → β a → m PUnit) (t : Raw α β cmp) : m PUnit :=
|
||||
t.inner.forM f
|
||||
|
|
@ -244,6 +277,11 @@ def toArray (t : Raw α β cmp) : Array ((a : α) × β a) :=
|
|||
def mergeWith [LawfulEqCmp cmp] (mergeFn : (a : α) → β a → β a → β a) (t₁ t₂ : Raw α β cmp) : Raw α β cmp :=
|
||||
letI : Ord α := ⟨cmp⟩; ⟨t₁.inner.mergeWith! mergeFn t₂.inner⟩
|
||||
|
||||
@[inline, inherit_doc mergeWith, deprecated mergeWith (since := "2025-02-12")]
|
||||
def mergeBy [LawfulEqCmp cmp] (mergeFn : (a : α) → β a → β a → β a) (t₁ t₂ : Raw α β cmp) :
|
||||
Raw α β cmp :=
|
||||
mergeWith mergeFn t₁ t₂
|
||||
|
||||
namespace Const
|
||||
open Internal (Impl)
|
||||
|
||||
|
|
@ -261,6 +299,10 @@ def toArray (t : Raw α β cmp) : Array (α × β) :=
|
|||
def mergeWith (mergeFn : α → β → β → β) (t₁ t₂ : Raw α β cmp) : Raw α β cmp :=
|
||||
letI : Ord α := ⟨cmp⟩; ⟨Impl.Const.mergeWith! mergeFn t₁.inner t₂.inner⟩
|
||||
|
||||
@[inline, inherit_doc mergeWith, deprecated mergeWith (since := "2025-02-12")]
|
||||
def mergeBy (mergeFn : α → β → β → β) (t₁ t₂ : Raw α β cmp) : Raw α β cmp :=
|
||||
mergeWith mergeFn t₁ t₂
|
||||
|
||||
end Const
|
||||
|
||||
@[inline, inherit_doc DTreeMap.eraseMany]
|
||||
|
|
|
|||
|
|
@ -129,6 +129,10 @@ def erase (t : TreeMap α β cmp) (a : α) : TreeMap α β cmp :=
|
|||
def get? (t : TreeMap α β cmp) (a : α) : Option β :=
|
||||
DTreeMap.Const.get? t.inner a
|
||||
|
||||
@[inline, inherit_doc get?, deprecated get? (since := "2025-02-12")]
|
||||
def find? (t : TreeMap α β cmp) (a : α) : Option β :=
|
||||
get? t a
|
||||
|
||||
@[inline, inherit_doc DTreeMap.get]
|
||||
def get (t : TreeMap α β cmp) (a : α) (h : a ∈ t) : β :=
|
||||
DTreeMap.Const.get t.inner a h
|
||||
|
|
@ -137,10 +141,18 @@ def get (t : TreeMap α β cmp) (a : α) (h : a ∈ t) : β :=
|
|||
def get! (t : TreeMap α β cmp) (a : α) [Inhabited β] : β :=
|
||||
DTreeMap.Const.get! t.inner a
|
||||
|
||||
@[inline, inherit_doc get!, deprecated get! (since := "2025-02-12")]
|
||||
def find! (t : TreeMap α β cmp) (a : α) [Inhabited β] : β :=
|
||||
get! t a
|
||||
|
||||
@[inline, inherit_doc DTreeMap.getD]
|
||||
def getD (t : TreeMap α β cmp) (a : α) (fallback : β) : β :=
|
||||
DTreeMap.Const.getD t.inner a fallback
|
||||
|
||||
@[inline, inherit_doc getD, deprecated getD (since := "2025-02-12")]
|
||||
def findD (t : TreeMap α β cmp) (a : α) (fallback : β) : β :=
|
||||
getD t a fallback
|
||||
|
||||
instance : GetElem? (TreeMap α β cmp) α β (fun m a => a ∈ m) where
|
||||
getElem m a h := m.get a h
|
||||
getElem? m a := m.get? a
|
||||
|
|
@ -156,10 +168,18 @@ def filter (f : α → β → Bool) (m : TreeMap α β cmp) : TreeMap α β cmp
|
|||
def foldlM (f : δ → (a : α) → β → m δ) (init : δ) (t : TreeMap α β cmp) : m δ :=
|
||||
t.inner.foldlM f init
|
||||
|
||||
@[inline, inherit_doc foldlM, deprecated foldlM (since := "2025-02-12")]
|
||||
def foldM (f : δ → (a : α) → β → m δ) (init : δ) (t : TreeMap α β cmp) : m δ :=
|
||||
t.foldlM f init
|
||||
|
||||
@[inline, inherit_doc DTreeMap.foldl]
|
||||
def foldl (f : δ → (a : α) → β → δ) (init : δ) (t : TreeMap α β cmp) : δ :=
|
||||
t.inner.foldl f init
|
||||
|
||||
@[inline, inherit_doc foldl, deprecated foldl (since := "2025-02-12")]
|
||||
def fold (f : δ → (a : α) → β → δ) (init : δ) (t : TreeMap α β cmp) : δ :=
|
||||
t.foldl f init
|
||||
|
||||
@[inline, inherit_doc DTreeMap.forM]
|
||||
def forM (f : α → β → m PUnit) (t : TreeMap α β cmp) : m PUnit :=
|
||||
t.inner.forM f
|
||||
|
|
@ -202,6 +222,10 @@ def toArray (t : TreeMap α β cmp) : Array (α × β) :=
|
|||
def mergeWith (mergeFn : α → β → β → β) (t₁ t₂ : TreeMap α β cmp) : TreeMap α β cmp :=
|
||||
⟨DTreeMap.Const.mergeWith mergeFn t₁.inner t₂.inner⟩
|
||||
|
||||
@[inline, inherit_doc mergeWith, deprecated mergeWith (since := "2025-02-12")]
|
||||
def mergeBy (mergeFn : α → β → β → β) (t₁ t₂ : TreeMap α β cmp) : TreeMap α β cmp :=
|
||||
mergeWith mergeFn t₁ t₂
|
||||
|
||||
@[inline, inherit_doc DTreeMap.eraseMany]
|
||||
def eraseMany {ρ} [ForIn Id ρ α] (t : TreeMap α β cmp) (l : ρ) : TreeMap α β cmp :=
|
||||
⟨t.inner.eraseMany l⟩
|
||||
|
|
|
|||
|
|
@ -147,6 +147,10 @@ def erase (t : Raw α β cmp) (a : α) : Raw α β cmp :=
|
|||
def get? (t : Raw α β cmp) (a : α) : Option β :=
|
||||
DTreeMap.Raw.Const.get? t.inner a
|
||||
|
||||
@[inline, inherit_doc get?, deprecated get? (since := "2025-02-12")]
|
||||
def find? (t : Raw α β cmp) (a : α) : Option β :=
|
||||
get? t a
|
||||
|
||||
@[inline, inherit_doc DTreeMap.Raw.Const.get]
|
||||
def get (t : Raw α β cmp) (a : α) (h : a ∈ t) : β :=
|
||||
DTreeMap.Raw.Const.get t.inner a h
|
||||
|
|
@ -155,10 +159,18 @@ def get (t : Raw α β cmp) (a : α) (h : a ∈ t) : β :=
|
|||
def get! (t : Raw α β cmp) (a : α) [Inhabited β] : β :=
|
||||
DTreeMap.Raw.Const.get! t.inner a
|
||||
|
||||
@[inline, inherit_doc get!, deprecated get! (since := "2025-02-12")]
|
||||
def find! (t : Raw α β cmp) (a : α) [Inhabited β] : β :=
|
||||
get! t a
|
||||
|
||||
@[inline, inherit_doc DTreeMap.Raw.Const.getD]
|
||||
def getD (t : Raw α β cmp) (a : α) (fallback : β) : β :=
|
||||
DTreeMap.Raw.Const.getD t.inner a fallback
|
||||
|
||||
@[inline, inherit_doc getD, deprecated getD (since := "2025-02-12")]
|
||||
def findD (t : Raw α β cmp) (a : α) (fallback : β) : β :=
|
||||
getD t a fallback
|
||||
|
||||
instance : GetElem? (Raw α β cmp) α β (fun m a => a ∈ m) where
|
||||
getElem m a h := m.get a h
|
||||
getElem? m a := m.get? a
|
||||
|
|
@ -174,10 +186,18 @@ def filter (f : α → β → Bool) (t : Raw α β cmp) : Raw α β cmp :=
|
|||
def foldlM (f : δ → (a : α) → β → m δ) (init : δ) (t : Raw α β cmp) : m δ :=
|
||||
t.inner.foldlM f init
|
||||
|
||||
@[inline, inherit_doc foldlM, deprecated foldlM (since := "2025-02-12")]
|
||||
def foldM (f : δ → (a : α) → β → m δ) (init : δ) (t : Raw α β cmp) : m δ :=
|
||||
t.foldlM f init
|
||||
|
||||
@[inline, inherit_doc DTreeMap.Raw.foldl]
|
||||
def foldl (f : δ → (a : α) → β → δ) (init : δ) (t : Raw α β cmp) : δ :=
|
||||
t.inner.foldl f init
|
||||
|
||||
@[inline, inherit_doc foldl, deprecated foldl (since := "2025-02-12")]
|
||||
def fold (f : δ → (a : α) → β → δ) (init : δ) (t : Raw α β cmp) : δ :=
|
||||
t.foldl f init
|
||||
|
||||
@[inline, inherit_doc DTreeMap.Raw.forM]
|
||||
def forM (f : α → β → m PUnit) (t : Raw α β cmp) : m PUnit :=
|
||||
t.inner.forM f
|
||||
|
|
@ -220,6 +240,10 @@ def toArray (t : Raw α β cmp) : Array (α × β) :=
|
|||
def mergeWith (mergeFn : α → β → β → β) (t₁ t₂ : Raw α β cmp) : Raw α β cmp :=
|
||||
⟨DTreeMap.Raw.Const.mergeWith mergeFn t₁.inner t₂.inner⟩
|
||||
|
||||
@[inline, inherit_doc mergeWith, deprecated mergeWith (since := "2025-02-12")]
|
||||
def mergeBy (mergeFn : α → β → β → β) (t₁ t₂ : Raw α β cmp) : Raw α β cmp :=
|
||||
mergeWith mergeFn t₁ t₂
|
||||
|
||||
@[inline, inherit_doc DTreeMap.Raw.eraseMany]
|
||||
def eraseMany {ρ} [ForIn Id ρ α] (t : Raw α β cmp) (l : ρ) : Raw α β cmp :=
|
||||
⟨t.inner.eraseMany l⟩
|
||||
|
|
|
|||
|
|
@ -162,11 +162,19 @@ ascending order.
|
|||
def foldlM {m δ} [Monad m] (f : δ → (a : α) → m δ) (init : δ) (t : TreeSet α cmp) : m δ :=
|
||||
t.inner.foldlM (fun c a _ => f c a) init
|
||||
|
||||
@[inline, inherit_doc foldlM, deprecated foldlM (since := "2025-02-12")]
|
||||
def foldM (f : δ → (a : α) → m δ) (init : δ) (t : TreeSet α cmp) : m δ :=
|
||||
t.foldlM f init
|
||||
|
||||
/-- Folds the given function over the elements of the tree set in ascending order. -/
|
||||
@[inline]
|
||||
def foldl (f : δ → (a : α) → δ) (init : δ) (t : TreeSet α cmp) : δ :=
|
||||
t.inner.foldl (fun c a _ => f c a) init
|
||||
|
||||
@[inline, inherit_doc foldl, deprecated foldl (since := "2025-02-12")]
|
||||
def fold (f : δ → (a : α) → δ) (init : δ) (t : TreeSet α cmp) : δ :=
|
||||
t.foldl f init
|
||||
|
||||
/-- Carries out a monadic action on each element in the tree set in ascending order. -/
|
||||
@[inline]
|
||||
def forM (f : α → m PUnit) (t : TreeSet α cmp) : m PUnit :=
|
||||
|
|
|
|||
|
|
@ -143,10 +143,18 @@ def filter (f : α → Bool) (t : Raw α cmp) : Raw α cmp :=
|
|||
def foldlM (f : δ → (a : α) → m δ) (init : δ) (t : Raw α cmp) : m δ :=
|
||||
t.inner.foldlM (fun c a _ => f c a) init
|
||||
|
||||
@[inline, inherit_doc foldlM, deprecated foldlM (since := "2025-02-12")]
|
||||
def foldM (f : δ → (a : α) → m δ) (init : δ) (t : Raw α cmp) : m δ :=
|
||||
t.foldlM f init
|
||||
|
||||
@[inline, inherit_doc TreeSet.empty]
|
||||
def foldl (f : δ → (a : α) → δ) (init : δ) (t : Raw α cmp) : δ :=
|
||||
t.inner.foldl (fun c a _ => f c a) init
|
||||
|
||||
@[inline, inherit_doc foldl, deprecated foldl (since := "2025-02-12")]
|
||||
def fold (f : δ → (a : α) → δ) (init : δ) (t : Raw α cmp) : δ :=
|
||||
t.foldl f init
|
||||
|
||||
@[inline, inherit_doc TreeSet.empty]
|
||||
def forM (f : α → m PUnit) (t : Raw α cmp) : m PUnit :=
|
||||
t.inner.forM (fun a _ => f a)
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue