def Lean.RBTree (α : Type u) (cmp : α → α → Ordering) : Type u

Equations

• Lean.RBTree α cmp = Lean.RBMap α Unit cmp

@[instance_reducible]

instance Lean.instInhabitedRBTree {α : Type u_1} {p : α → α → Ordering} : Inhabited (RBTree α p)

Equations

• Lean.instInhabitedRBTree = { default := Lean.RBMap.empty }

@[inline]

def Lean.mkRBTree (α : Type u) (cmp : α → α → Ordering) : RBTree α cmp

Equations

• Lean.mkRBTree α cmp = Lean.mkRBMap α Unit cmp

@[instance_reducible]

instance Lean.instEmptyCollectionRBTree (α : Type u) (cmp : α → α → Ordering) : EmptyCollection (RBTree α cmp)

Equations

• Lean.instEmptyCollectionRBTree α cmp = { emptyCollection := Lean.mkRBTree α cmp }

@[inline]

def Lean.RBTree.empty {α : Type u} {cmp : α → α → Ordering} : RBTree α cmp

Equations

• Lean.RBTree.empty = Lean.RBMap.empty

@[inline]

def Lean.RBTree.depth {α : Type u} {cmp : α → α → Ordering} (f : Nat → Nat → Nat) (t : RBTree α cmp) : Nat

Equations

• Lean.RBTree.depth f t = Lean.RBMap.depth f t

@[inline]

def Lean.RBTree.fold {α : Type u} {β : Type v} {cmp : α → α → Ordering} (f : β → α → β) (init : β) (t : RBTree α cmp) : β

Equations

• Lean.RBTree.fold f init t = Lean.RBMap.fold (fun (r : β) (a : α) (x : Unit) => f r a) init t

@[inline]

def Lean.RBTree.revFold {α : Type u} {β : Type v} {cmp : α → α → Ordering} (f : β → α → β) (init : β) (t : RBTree α cmp) : β

Equations

• Lean.RBTree.revFold f init t = Lean.RBMap.revFold (fun (r : β) (a : α) (x : Unit) => f r a) init t

@[inline]

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

Equations

• Lean.RBTree.foldM f init t = Lean.RBMap.foldM (fun (r : β) (a : α) (x : Unit) => f r a) init t

@[inline]

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

Equations

• Lean.RBTree.forM f t = Lean.RBTree.foldM (fun (x : PUnit) (a : α) => f a) PUnit.unit t

@[inline]

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

Equations

• t.forIn init f = t.val.forIn init fun (a : α) (x : Unit) (acc : σ) => f a acc

@[instance_reducible]

instance Lean.RBTree.instForInOfMonad {α : Type u} {cmp : α → α → Ordering} {m : Type u_1 → Type u_2} [Monad m] : ForIn m (RBTree α cmp) α

Equations

• Lean.RBTree.instForInOfMonad = { forIn := fun {β : Type ?u.2} => Lean.RBTree.forIn }

@[inline]

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

Equations

• t.isEmpty = Lean.RBMap.isEmpty t

@[specialize #[]]

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

Equations

• t.toList = Lean.RBTree.revFold (fun (as : List α) (a : α) => a :: as) [] t

@[specialize #[]]

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

Equations

• t.toArray = Lean.RBTree.fold (fun (as : Array α) (a : α) => as.push a) #[] t

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[instance_reducible]

instance Lean.RBTree.instRepr {α : Type u} {cmp : α → α → Ordering} [Repr α] : Repr (RBTree α cmp)

Equations

• Lean.RBTree.instRepr = { reprPrec := fun (t : Lean.RBTree α cmp) (prec : Nat) => Repr.addAppParen (Std.Format.text "Lean.rbtreeOf " ++ repr t.toList) prec }

@[inline]

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

Equations

• t.insert a = Lean.RBMap.insert t a ()

@[inline]

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

Equations

• t.erase a = Lean.RBMap.erase t a

@[specialize #[]]

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

Equations

• Lean.RBTree.ofList [] = Lean.mkRBTree α cmp
• Lean.RBTree.ofList (x_1 :: xs) = (Lean.RBTree.ofList xs).insert x_1

@[inline]

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

Equations

• t.find? a = match Lean.RBMap.findCore? t a with | some ⟨a, snd⟩ => some a | none => none

@[inline]

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

Equations

• t.contains a = (t.find? a).isSome

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

Equations

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

def Lean.RBTree.fromArray {α : Type u} (l : Array α) (cmp : α → α → Ordering) : RBTree α cmp

Equations

• Lean.RBTree.fromArray l cmp = Array.foldl Lean.RBTree.insert (Lean.mkRBTree α cmp) l

@[inline]

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

Equations

• t.all p = Lean.RBMap.all t fun (a : α) (x : Unit) => p a

@[inline]

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

Equations

• t.any p = Lean.RBMap.any t fun (a : α) (x : Unit) => p a

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

Equations

• t₁.subset t₂ = t₁.all fun (a : α) => (t₂.find? a).isSome

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

Equations

• t₁.seteq t₂ = (t₁.subset t₂ && t₂.subset t₁)

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

Equations

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

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

Equations

• t₁.diff t₂ = Lean.RBTree.fold Lean.RBTree.erase t₁ t₂

def Lean.RBTree.filter {α : Type u} {cmp : α → α → Ordering} (f : α → Bool) (m : RBTree α cmp) : RBTree α cmp

filter f m returns the RBTree consisting of all x in m where f x returns true.

Equations

• Lean.RBTree.filter f m = Lean.RBMap.filter (fun (a : α) (x : Unit) => f a) m

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

Equations

• Lean.rbtreeOf l cmp = Lean.RBTree.fromList l cmp