Equations
- Std.RBTree α cmp = Std.RBMap α Unit cmp
Equations
- Std.instInhabitedRBTree = { default := Std.RBMap.empty }
@[inline]
Equations
- Std.mkRBTree α cmp = Std.mkRBMap α Unit cmp
instance
Std.instEmptyCollectionRBTree
(α : Type u)
(cmp : α → α → Ordering)
:
EmptyCollection (Std.RBTree α cmp)
Equations
- Std.instEmptyCollectionRBTree α cmp = { emptyCollection := Std.mkRBTree α cmp }
@[inline]
Equations
- Std.RBTree.empty = Std.RBMap.empty
@[inline]
def
Std.RBTree.depth
{α : Type u}
{cmp : α → α → Ordering}
(f : Nat → Nat → Nat)
(t : Std.RBTree α cmp)
:
Equations
- Std.RBTree.depth f t = Std.RBMap.depth f t
@[inline]
def
Std.RBTree.fold
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
(f : β → α → β)
(init : β)
(t : Std.RBTree α cmp)
:
β
Equations
- Std.RBTree.fold f init t = Std.RBMap.fold (fun r a x => f r a) init t
@[inline]
def
Std.RBTree.revFold
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
(f : β → α → β)
(init : β)
(t : Std.RBTree α cmp)
:
β
Equations
- Std.RBTree.revFold f init t = Std.RBMap.revFold (fun r a x => f r a) init t
@[inline]
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
@[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
@[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
instance
Std.RBTree.instForInRBTree
{α : Type u}
{cmp : α → α → Ordering}
{m : Type u_1 → Type u_2}
:
ForIn m (Std.RBTree α cmp) α
@[inline]
Equations
@[specialize]
Equations
- Std.RBTree.toList t = Std.RBTree.revFold (fun as a => a :: as) [] t
@[specialize]
Equations
- Std.RBTree.toArray t = Std.RBTree.fold (fun as a => Array.push as a) #[] t
@[inline]
Equations
- Std.RBTree.min t = match Std.RBMap.min t with | some (a, x) => some a | none => none
@[inline]
Equations
- Std.RBTree.max t = match Std.RBMap.max t with | some (a, x) => some a | none => none
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 }
@[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 ()
@[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
@[specialize]
Equations
- Std.RBTree.ofList [] = Std.mkRBTree α cmp
- Std.RBTree.ofList (x_1 :: xs) = Std.RBTree.insert (Std.RBTree.ofList xs) x_1
@[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 := x } => some a | none => none
@[inline]
Equations
- Std.RBTree.contains t a = Option.isSome (Std.RBTree.find? t a)
Equations
- Std.RBTree.fromList l cmp = List.foldl Std.RBTree.insert (Std.mkRBTree α cmp) l
@[inline]
Equations
- Std.RBTree.all t p = Std.RBMap.all t fun a x => p a
@[inline]
Equations
- Std.RBTree.any t p = Std.RBMap.any t fun a x => p a
def
Std.RBTree.subset
{α : Type u}
{cmp : α → α → Ordering}
(t₁ : Std.RBTree α cmp)
(t₂ : Std.RBTree α cmp)
:
Equations
- Std.RBTree.subset t₁ t₂ = Std.RBTree.all t₁ fun a => Option.toBool (Std.RBTree.find? t₂ a)
def
Std.RBTree.seteq
{α : Type u}
{cmp : α → α → Ordering}
(t₁ : Std.RBTree α cmp)
(t₂ : Std.RBTree α cmp)
:
Equations
- Std.RBTree.seteq t₁ t₂ = (Std.RBTree.subset t₁ t₂ && Std.RBTree.subset t₂ t₁)
Equations
- Std.rbtreeOf l cmp = Std.RBTree.fromList l cmp