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

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

@[inline]

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

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[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 β

@[inline]

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

@[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 σ

instance Lean.RBTree.instForIn {α : Type u} {cmp : α → α → Ordering} {m : Type u_1 → Type u_2} : ForIn m (RBTree α cmp) α

@[inline]

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

@[specialize #[]]

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

@[specialize #[]]

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

@[inline]

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

@[inline]

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

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

@[inline]

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

@[inline]

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

@[specialize #[]]

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

@[inline]

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

@[inline]

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

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

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

@[inline]

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

@[inline]

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

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

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

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

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

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.

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