Std.Data.RBTree

def Std.RBTree.foldM {α : Type u} {β : Type v} {cmp : α → α → Ordering} {m : Type v → Type w} [inst : Monad m] (f : β → α → m β) (init : β) (t : Std.RBTree α cmp) :

m β

Equations

Std.RBTree.foldM f init t = Std.RBMap.foldM (fun r a x => f r a) init t

source

@[inline]

def Std.RBTree.forM {α : Type u} {cmp : α → α → Ordering} {m : Type v → Type w} [inst : Monad m] (f : α → m PUnit) (t : Std.RBTree α cmp) :

m PUnit

Equations

Std.RBTree.forM f t = Std.RBTree.foldM (fun x a => f a) PUnit.unit t

source

@[inline]

def Std.RBTree.forIn {α : Type u} {cmp : α → α → Ordering} {m : Type u_1 → Type u_2} {σ : Type u_1} [inst : Monad m] (t : Std.RBTree α cmp) (init : σ) (f : α → σ → m (ForInStep σ)) :

m σ

Equations

Std.RBTree.forIn t init f = Std.RBNode.forIn t.val init fun a x acc => f a acc

source

instance Std.RBTree.instForInRBTree {α : Type u} {cmp : α → α → Ordering} {m : Type u_1 → Type u_2} :

ForIn m (Std.RBTree α cmp) α

Equations

Std.RBTree.instForInRBTree = { forIn := fun {β} [Monad m] => Std.RBTree.forIn }

source

@[inline]

def Std.RBTree.isEmpty {α : Type u} {cmp : α → α → Ordering} (t : Std.RBTree α cmp) :

Bool

Equations

Std.RBTree.isEmpty t = Std.RBMap.isEmpty t

source

@[specialize]

def Std.RBTree.toList {α : Type u} {cmp : α → α → Ordering} (t : Std.RBTree α cmp) :

List α

Equations

Std.RBTree.toList t = Std.RBTree.revFold (fun as a => a :: as) [] t

source

@[specialize]

def Std.RBTree.toArray {α : Type u} {cmp : α → α → Ordering} (t : Std.RBTree α cmp) :

Array α

Equations

Std.RBTree.toArray t = Std.RBTree.fold (fun as a => Array.push as a) #[] t

source

@[inline]

def Std.RBTree.min {α : Type u} {cmp : α → α → Ordering} (t : Std.RBTree α cmp) :

Option α

Equations

Std.RBTree.min t = match Std.RBMap.min t with | some (a, snd) => some a | none => none

source

@[inline]

def Std.RBTree.max {α : Type u} {cmp : α → α → Ordering} (t : Std.RBTree α cmp) :

Option α

Equations

Std.RBTree.max t = match Std.RBMap.max t with | some (a, snd) => some a | none => none

source

instance Std.RBTree.instReprRBTree {α : Type u} {cmp : α → α → Ordering} [inst : Repr α] :

Repr (Std.RBTree α cmp)

Equations

Std.RBTree.instReprRBTree = { reprPrec := fun t prec => Repr.addAppParen (Std.Format.text "Std.rbtreeOf " ++ repr (Std.RBTree.toList t)) prec }

source

@[inline]

def Std.RBTree.insert {α : Type u} {cmp : α → α → Ordering} (t : Std.RBTree α cmp) (a : α) :

Std.RBTree α cmp

Equations

Std.RBTree.insert t a = Std.RBMap.insert t a ()

source

@[inline]

def Std.RBTree.erase {α : Type u} {cmp : α → α → Ordering} (t : Std.RBTree α cmp) (a : α) :

Std.RBTree α cmp

Equations

Std.RBTree.erase t a = Std.RBMap.erase t a

source

@[specialize]

def Std.RBTree.ofList {α : Type u} {cmp : α → α → Ordering} :

List α → Std.RBTree α cmp

Equations

Std.RBTree.ofList [] = Std.mkRBTree α cmp
Std.RBTree.ofList (x :: xs) = Std.RBTree.insert (Std.RBTree.ofList xs) x

source

@[inline]

def Std.RBTree.find? {α : Type u} {cmp : α → α → Ordering} (t : Std.RBTree α cmp) (a : α) :

Option α

Equations

Std.RBTree.find? t a = match Std.RBMap.findCore? t a with | some { fst := a, snd := snd } => some a | none => none

source

@[inline]

def Std.RBTree.contains {α : Type u} {cmp : α → α → Ordering} (t : Std.RBTree α cmp) (a : α) :

Bool

Equations

Std.RBTree.contains t a = Option.isSome (Std.RBTree.find? t a)

source

def Std.RBTree.fromList {α : Type u} (l : List α) (cmp : α → α → Ordering) :

Std.RBTree α cmp

Equations

Std.RBTree.fromList l cmp = List.foldl Std.RBTree.insert (Std.mkRBTree α cmp) l

source

@[inline]

def Std.RBTree.all {α : Type u} {cmp : α → α → Ordering} (t : Std.RBTree α cmp) (p : α → Bool) :

Bool

Equations

Std.RBTree.all t p = Std.RBMap.all t fun a x => p a

source

@[inline]

def Std.RBTree.any {α : Type u} {cmp : α → α → Ordering} (t : Std.RBTree α cmp) (p : α → Bool) :

Bool

Equations

Std.RBTree.any t p = Std.RBMap.any t fun a x => p a

source

def Std.RBTree.subset {α : Type u} {cmp : α → α → Ordering} (t₁ : Std.RBTree α cmp) (t₂ : Std.RBTree α cmp) :

Bool

Equations

Std.RBTree.subset t₁ t₂ = Std.RBTree.all t₁ fun a => Option.toBool (Std.RBTree.find? t₂ a)

source

def Std.RBTree.seteq {α : Type u} {cmp : α → α → Ordering} (t₁ : Std.RBTree α cmp) (t₂ : Std.RBTree α cmp) :

Bool

Equations

Std.RBTree.seteq t₁ t₂ = (Std.RBTree.subset t₁ t₂ && Std.RBTree.subset t₂ t₁)

source

def Std.RBTree.union {α : Type u} {cmp : α → α → Ordering} (t₁ : Std.RBTree α cmp) (t₂ : Std.RBTree α cmp) :

Std.RBTree α cmp

Equations

Std.RBTree.union t₁ t₂ = if Std.RBTree.isEmpty t₁ = true then t₂ else Std.RBTree.fold Std.RBTree.insert t₁ t₂

source

def Std.RBTree.diff {α : Type u} {cmp : α → α → Ordering} (t₁ : Std.RBTree α cmp) (t₂ : Std.RBTree α cmp) :

Std.RBTree α cmp

Equations

Std.RBTree.diff t₁ t₂ = Std.RBTree.fold Std.RBTree.erase t₁ t₂

source

def Std.rbtreeOf {α : Type u} (l : List α) (cmp : α → α → Ordering) :

Std.RBTree α cmp

Equations

Std.rbtreeOf l cmp = Std.RBTree.fromList l cmp