inductive Lean.RBColor : Type

• red : RBColor
• black : RBColor

inductive Lean.RBNode (α : Type u) (β : α → Type v) : Type (max u v)

• leaf {α : Type u} {β : α → Type v} : RBNode α β
• node {α : Type u} {β : α → Type v} (color : RBColor) (lchild : RBNode α β) (key : α) (val : β key) (rchild : RBNode α β) : RBNode α β

def Lean.RBNode.depth {α : Type u} {β : α → Type v} (f : Nat → Nat → Nat) : RBNode α β → Nat

def Lean.RBNode.min {α : Type u} {β : α → Type v} : RBNode α β → Option ((k : α) × β k)

def Lean.RBNode.max {α : Type u} {β : α → Type v} : RBNode α β → Option ((k : α) × β k)

@[specialize #[]]

def Lean.RBNode.fold {α : Type u} {β : α → Type v} {σ : Type w} (f : σ → (k : α) → β k → σ) (init : σ) : RBNode α β → σ

@[specialize #[]]

def Lean.RBNode.forM {α : Type u} {β : α → Type v} {m : Type → Type u_1} [Monad m] (f : (k : α) → β k → m Unit) : RBNode α β → m Unit

@[specialize #[]]

def Lean.RBNode.foldM {α : Type u} {β : α → Type v} {σ : Type w} {m : Type w → Type u_1} [Monad m] (f : σ → (k : α) → β k → m σ) (init : σ) : RBNode α β → m σ

@[inline]

def Lean.RBNode.forIn {α : Type u} {β : α → Type v} {σ : Type w} {m : Type w → Type u_1} [Monad m] (as : RBNode α β) (init : σ) (f : (k : α) → β k → σ → m (ForInStep σ)) : m σ

@[specialize #[]]

def Lean.RBNode.forIn.visit {α : Type u} {β : α → Type v} {σ : Type w} {m : Type w → Type u_1} [Monad m] (f : (k : α) → β k → σ → m (ForInStep σ)) : RBNode α β → σ → m (ForInStep σ)

@[specialize #[]]

def Lean.RBNode.revFold {α : Type u} {β : α → Type v} {σ : Type w} (f : σ → (k : α) → β k → σ) (init : σ) : RBNode α β → σ

@[specialize #[]]

def Lean.RBNode.all {α : Type u} {β : α → Type v} (p : (k : α) → β k → Bool) : RBNode α β → Bool

@[specialize #[]]

def Lean.RBNode.any {α : Type u} {β : α → Type v} (p : (k : α) → β k → Bool) : RBNode α β → Bool

def Lean.RBNode.singleton {α : Type u} {β : α → Type v} (k : α) (v : β k) : RBNode α β

def Lean.RBNode.isSingleton {α : Type u} {β : α → Type v} : RBNode α β → Bool

@[inline]

def Lean.RBNode.balance1 {α : Type u} {β : α → Type v} : RBNode α β → (a : α) → β a → RBNode α β → RBNode α β

@[inline]

def Lean.RBNode.balance2 {α : Type u} {β : α → Type v} : RBNode α β → (a : α) → β a → RBNode α β → RBNode α β

def Lean.RBNode.isRed {α : Type u} {β : α → Type v} : RBNode α β → Bool

def Lean.RBNode.isBlack {α : Type u} {β : α → Type v} : RBNode α β → Bool

@[specialize #[]]

def Lean.RBNode.ins {α : Type u} {β : α → Type v} (cmp : α → α → Ordering) : RBNode α β → (k : α) → β k → RBNode α β

def Lean.RBNode.setBlack {α : Type u} {β : α → Type v} : RBNode α β → RBNode α β

@[specialize #[]]

def Lean.RBNode.insert {α : Type u} {β : α → Type v} (cmp : α → α → Ordering) (t : RBNode α β) (k : α) (v : β k) : RBNode α β

def Lean.RBNode.setRed {α : Type u} {β : α → Type v} : RBNode α β → RBNode α β

def Lean.RBNode.balLeft {α : Type u} {β : α → Type v} : RBNode α β → (k : α) → β k → RBNode α β → RBNode α β

def Lean.RBNode.balRight {α : Type u} {β : α → Type v} (l : RBNode α β) (k : α) (v : β k) (r : RBNode α β) : RBNode α β

def Lean.RBNode.size {α : Type u} {β : α → Type v} : RBNode α β → Nat

The number of nodes in the tree.

@[irreducible]

def Lean.RBNode.appendTrees {α : Type u} {β : α → Type v} : RBNode α β → RBNode α β → RBNode α β

@[specialize #[]]

def Lean.RBNode.del {α : Type u} {β : α → Type v} (cmp : α → α → Ordering) (x : α) : RBNode α β → RBNode α β

@[specialize #[]]

def Lean.RBNode.erase {α : Type u} {β : α → Type v} (cmp : α → α → Ordering) (x : α) (t : RBNode α β) : RBNode α β

@[specialize #[]]

def Lean.RBNode.findCore {α : Type u} {β : α → Type v} (cmp : α → α → Ordering) : RBNode α β → (k : α) → Option ((k : α) × β k)

@[specialize #[]]

def Lean.RBNode.find {α : Type u} (cmp : α → α → Ordering) {β : Type v} : (RBNode α fun (x : α) => β) → α → Option β

@[specialize #[]]

def Lean.RBNode.lowerBound {α : Type u} {β : α → Type v} (cmp : α → α → Ordering) : RBNode α β → α → Option (Sigma β) → Option (Sigma β)

inductive Lean.RBNode.WellFormed {α : Type u} {β : α → Type v} (cmp : α → α → Ordering) : RBNode α β → Prop

• leafWff {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} : WellFormed cmp leaf
• insertWff {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {n n' : RBNode α β} {k : α} {v : β k} : WellFormed cmp n → n' = insert cmp n k v → WellFormed cmp n'
• eraseWff {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {n n' : RBNode α β} {k : α} : WellFormed cmp n → n' = erase cmp k n → WellFormed cmp n'

@[specialize #[]]

def Lean.RBNode.mapM {α : Type v} {β γ : α → Type v} {M : Type v → Type v} [Applicative M] (f : (a : α) → β a → M (γ a)) : RBNode α β → M (RBNode α γ)

@[specialize #[]]

def Lean.RBNode.map {α : Type u} {β γ : α → Type v} (f : (a : α) → β a → γ a) : RBNode α β → RBNode α γ

def Lean.RBNode.toArray {α : Type u} {β : α → Type v} (n : RBNode α β) : Array (Sigma β)

instance Lean.RBNode.instEmptyCollection {α : Type u} {β : α → Type v} : EmptyCollection (RBNode α β)

def Lean.RBMap (α : Type u) (β : Type v) (cmp : α → α → Ordering) : Type (max u v)

@[inline]

def Lean.mkRBMap (α : Type u) (β : Type v) (cmp : α → α → Ordering) : RBMap α β cmp

@[inline]

def Lean.RBMap.empty {α : Type u} {β : Type v} {cmp : α → α → Ordering} : RBMap α β cmp

instance Lean.instEmptyCollectionRBMap (α : Type u) (β : Type v) (cmp : α → α → Ordering) : EmptyCollection (RBMap α β cmp)

instance Lean.instInhabitedRBMap (α : Type u) (β : Type v) (cmp : α → α → Ordering) : Inhabited (RBMap α β cmp)

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

def Lean.RBMap.isSingleton {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : RBMap α β cmp) : Bool

@[inline]

def Lean.RBMap.fold {α : Type u} {β : Type v} {σ : Type w} {cmp : α → α → Ordering} (f : σ → α → β → σ) (init : σ) : RBMap α β cmp → σ

@[inline]

def Lean.RBMap.revFold {α : Type u} {β : Type v} {σ : Type w} {cmp : α → α → Ordering} (f : σ → α → β → σ) (init : σ) : RBMap α β cmp → σ

@[inline]

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

@[inline]

def Lean.RBMap.forM {α : Type u} {β : Type v} {cmp : α → α → Ordering} {m : Type u_1 → Type u_2} [Monad m] (f : α → β → m PUnit) (t : RBMap α β cmp) : m PUnit

@[inline]

def Lean.RBMap.forIn {α : Type u} {β : Type v} {σ : Type w} {cmp : α → α → Ordering} {m : Type w → Type u_1} [Monad m] (t : RBMap α β cmp) (init : σ) (f : α × β → σ → m (ForInStep σ)) : m σ

instance Lean.RBMap.instForInProd {α : Type u} {β : Type v} {cmp : α → α → Ordering} {m : Type u_1 → Type u_2} : ForIn m (RBMap α β cmp) (α × β)

@[inline]

def Lean.RBMap.isEmpty {α : Type u} {β : Type v} {cmp : α → α → Ordering} : RBMap α β cmp → Bool

@[specialize #[]]

def Lean.RBMap.toList {α : Type u} {β : Type v} {cmp : α → α → Ordering} : RBMap α β cmp → List (α × β)

Returns a List of the key/value pairs in order.

@[specialize #[]]

def Lean.RBMap.toArray {α : Type u} {β : Type v} {cmp : α → α → Ordering} : RBMap α β cmp → Array (α × β)

Returns an Array of the key/value pairs in order.

@[inline]

def Lean.RBMap.min {α : Type u} {β : Type v} {cmp : α → α → Ordering} : RBMap α β cmp → Option (α × β)

Returns the kv pair (a,b) such that a ≤ k for all keys in the RBMap.

@[inline]

def Lean.RBMap.max {α : Type u} {β : Type v} {cmp : α → α → Ordering} : RBMap α β cmp → Option (α × β)

Returns the kv pair (a,b) such that a ≥ k for all keys in the RBMap.

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

@[inline]

def Lean.RBMap.insert {α : Type u} {β : Type v} {cmp : α → α → Ordering} : RBMap α β cmp → α → β → RBMap α β cmp

@[inline]

def Lean.RBMap.erase {α : Type u} {β : Type v} {cmp : α → α → Ordering} : RBMap α β cmp → α → RBMap α β cmp

@[specialize #[]]

def Lean.RBMap.ofList {α : Type u} {β : Type v} {cmp : α → α → Ordering} : List (α × β) → RBMap α β cmp

@[inline]

def Lean.RBMap.findCore? {α : Type u} {β : Type v} {cmp : α → α → Ordering} : RBMap α β cmp → α → Option ((_ : α) × β)

@[inline]

def Lean.RBMap.find? {α : Type u} {β : Type v} {cmp : α → α → Ordering} : RBMap α β cmp → α → Option β

@[inline]

def Lean.RBMap.findD {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : RBMap α β cmp) (k : α) (v₀ : β) : β

@[inline]

def Lean.RBMap.lowerBound {α : Type u} {β : Type v} {cmp : α → α → Ordering} : RBMap α β cmp → α → Option ((_ : α) × β)

(lowerBound k) retrieves the kv pair of the largest key smaller than or equal to k, if it exists.

@[inline]

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

Returns true if the given key a is in the RBMap.

@[inline]

def Lean.RBMap.fromList {α : Type u} {β : Type v} (l : List (α × β)) (cmp : α → α → Ordering) : RBMap α β cmp

@[inline]

def Lean.RBMap.fromArray {α : Type u} {β : Type v} (l : Array (α × β)) (cmp : α → α → Ordering) : RBMap α β cmp

@[inline]

def Lean.RBMap.all {α : Type u} {β : Type v} {cmp : α → α → Ordering} : RBMap α β cmp → (α → β → Bool) → Bool

Returns true if the given predicate is true for all items in the RBMap.

@[inline]

def Lean.RBMap.any {α : Type u} {β : Type v} {cmp : α → α → Ordering} : RBMap α β cmp → (α → β → Bool) → Bool

Returns true if the given predicate is true for any item in the RBMap.

def Lean.RBMap.size {α : Type u} {β : Type v} {cmp : α → α → Ordering} (m : RBMap α β cmp) : Nat

The number of items in the RBMap.

def Lean.RBMap.maxDepth {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : RBMap α β cmp) : Nat

@[inline]

def Lean.RBMap.min! {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Inhabited α] [Inhabited β] (t : RBMap α β cmp) : α × β

@[inline]

def Lean.RBMap.max! {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Inhabited α] [Inhabited β] (t : RBMap α β cmp) : α × β

@[inline]

def Lean.RBMap.find! {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Inhabited β] (t : RBMap α β cmp) (k : α) : β

Attempts to find the value with key k : α in t and panics if there is no such key.

def Lean.RBMap.mergeBy {α : Type u} {β : Type v} {cmp : α → α → Ordering} (mergeFn : α → β → β → β) (t₁ t₂ : RBMap α β cmp) : RBMap α β cmp

Merges the maps t₁ and t₂, if a key a : α exists in both, then use mergeFn a b₁ b₂ to produce the new merged value.

def Lean.RBMap.intersectBy {α : Type u} {β : Type v} {cmp : α → α → Ordering} {γ : Type v₁} {δ : Type v₂} (mergeFn : α → β → γ → δ) (t₁ : RBMap α β cmp) (t₂ : RBMap α γ cmp) : RBMap α δ cmp

Intersects the maps t₁ and t₂ using mergeFn a b₁ b₂ to produce the new value.

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

filter f m returns the RBMap consisting of all "key/val"-pairs in m where f key val returns true.

def Lean.RBMap.filterMap {α : Type u} {β : Type v} {cmp : α → α → Ordering} {γ : Type u_1} (f : α → β → Option γ) (m : RBMap α β cmp) : RBMap α γ cmp

filterMap f m filters an RBMap and simultaneously modifies the filtered values.

It takes a function f : α → β → Option γ and applies f k v to the value with key k. The resulting entries with non-none value are collected to form the output RBMap.

def Lean.rbmapOf {α : Type u} {β : Type v} (l : List (α × β)) (cmp : α → α → Ordering) : RBMap α β cmp