inductive Lean.RBColor : Type

• red: Lean.RBColor
• black: Lean.RBColor

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

• leaf: {α : Type u} → {β : α → Type v} → Lean.RBNode α β
• node: {α : Type u} → {β : α → Type v} → Lean.RBColor → Lean.RBNode α β → (key : α) → β key → Lean.RBNode α β → Lean.RBNode α β

Instances For

• Lean.Json.instCoeRBNodeStringJsonStructured
• Lean.RBNode.instEmptyCollectionRBNode

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

Equations

• Lean.RBNode.depth f Lean.RBNode.leaf = 0
• Lean.RBNode.depth f (Lean.RBNode.node color l key val r) = Nat.succ (f (Lean.RBNode.depth f l) (Lean.RBNode.depth f r))

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

Equations

• Lean.RBNode.min Lean.RBNode.leaf = none
• Lean.RBNode.min (Lean.RBNode.node color Lean.RBNode.leaf k v rchild) = some { fst := k, snd := v }
• Lean.RBNode.min (Lean.RBNode.node color l key val rchild) = Lean.RBNode.min l

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

Equations

• Lean.RBNode.max Lean.RBNode.leaf = none
• Lean.RBNode.max (Lean.RBNode.node color lchild k v Lean.RBNode.leaf) = some { fst := k, snd := v }
• Lean.RBNode.max (Lean.RBNode.node color lchild key val r) = Lean.RBNode.max r

@[specialize #[]]

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

Equations

• Lean.RBNode.fold f x Lean.RBNode.leaf = x
• Lean.RBNode.fold f x (Lean.RBNode.node color l k v r) = Lean.RBNode.fold f (f (Lean.RBNode.fold f x l) k v) r

@[specialize #[]]

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

Equations

• Lean.RBNode.forM f Lean.RBNode.leaf = pure ()
• Lean.RBNode.forM f (Lean.RBNode.node color l key val r) = do Lean.RBNode.forM f l f key val Lean.RBNode.forM f r

@[specialize #[]]

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

Equations

• Lean.RBNode.foldM f x Lean.RBNode.leaf = pure x
• Lean.RBNode.foldM f x (Lean.RBNode.node color l k v r) = do let b ← Lean.RBNode.foldM f x l let b ← f b k v Lean.RBNode.foldM f b r

@[inline]

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

Equations

• Lean.RBNode.forIn as init f = do let __do_lift ← Lean.RBNode.forIn.visit f as init match __do_lift with | ForInStep.done b => pure b | ForInStep.yield b => pure b

@[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 σ)) : Lean.RBNode α β → σ → m (ForInStep σ)

Equations

• One or more equations did not get rendered due to their size.
• Lean.RBNode.forIn.visit f Lean.RBNode.leaf x = pure (ForInStep.yield x)

@[specialize #[]]

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

Equations

• Lean.RBNode.revFold f x Lean.RBNode.leaf = x
• Lean.RBNode.revFold f x (Lean.RBNode.node color l k v r) = Lean.RBNode.revFold f (f (Lean.RBNode.revFold f x r) k v) l

@[specialize #[]]

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

Equations

• Lean.RBNode.all p Lean.RBNode.leaf = true
• Lean.RBNode.all p (Lean.RBNode.node color l key val r) = (p key val && Lean.RBNode.all p l && Lean.RBNode.all p r)

@[specialize #[]]

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

Equations

• Lean.RBNode.any p Lean.RBNode.leaf = false
• Lean.RBNode.any p (Lean.RBNode.node color l key val r) = (p key val || Lean.RBNode.any p l || Lean.RBNode.any p r)

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

Equations

• Lean.RBNode.singleton k v = Lean.RBNode.node Lean.RBColor.red Lean.RBNode.leaf k v Lean.RBNode.leaf

@[inline]

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

Equations

• One or more equations did not get rendered due to their size.

@[inline]

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.RBNode.isRed x = match x with | Lean.RBNode.node Lean.RBColor.red lchild key val rchild => true | x => false

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

Equations

• Lean.RBNode.isBlack x = match x with | Lean.RBNode.node Lean.RBColor.black lchild key val rchild => true | x => false

@[specialize #[]]

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.RBNode.ins cmp Lean.RBNode.leaf x✝ x = Lean.RBNode.node Lean.RBColor.red Lean.RBNode.leaf x✝ x Lean.RBNode.leaf

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

Equations

• Lean.RBNode.setBlack x = match x with | Lean.RBNode.node color l k v r => Lean.RBNode.node Lean.RBColor.black l k v r | e => e

@[specialize #[]]

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

Equations

• Lean.RBNode.insert cmp t k v = if Lean.RBNode.isRed t = true then Lean.RBNode.setBlack (Lean.RBNode.ins cmp t k v) else Lean.RBNode.ins cmp t k v

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

Equations

• Lean.RBNode.setRed x = match x with | Lean.RBNode.node color a k v b => Lean.RBNode.node Lean.RBColor.red a k v b | e => e

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

The number of nodes in the tree.

Equations

• Lean.RBNode.size Lean.RBNode.leaf = 0
• Lean.RBNode.size (Lean.RBNode.node color l key val r) = Lean.RBNode.size l + Lean.RBNode.size r + 1

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.RBNode.appendTrees Lean.RBNode.leaf x = x
• Lean.RBNode.appendTrees x Lean.RBNode.leaf = x
• Lean.RBNode.appendTrees x (Lean.RBNode.node Lean.RBColor.red b kx vx c) = Lean.RBNode.node Lean.RBColor.red (Lean.RBNode.appendTrees x b) kx vx c
• Lean.RBNode.appendTrees (Lean.RBNode.node Lean.RBColor.red a kx vx b) x = Lean.RBNode.node Lean.RBColor.red a kx vx (Lean.RBNode.appendTrees b x)

@[specialize #[]]

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.RBNode.del cmp x Lean.RBNode.leaf = Lean.RBNode.leaf

@[specialize #[]]

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

Equations

• Lean.RBNode.erase cmp x t = let t := Lean.RBNode.del cmp x t; Lean.RBNode.setBlack t

@[specialize #[]]

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.RBNode.findCore cmp Lean.RBNode.leaf x = none

@[specialize #[]]

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.RBNode.find cmp Lean.RBNode.leaf x = none

@[specialize #[]]

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.RBNode.lowerBound cmp Lean.RBNode.leaf x✝ x = x

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

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

@[specialize #[]]

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.RBNode.mapM f Lean.RBNode.leaf = pure Lean.RBNode.leaf

@[specialize #[]]

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

Equations

• Lean.RBNode.map f Lean.RBNode.leaf = Lean.RBNode.leaf
• Lean.RBNode.map f (Lean.RBNode.node color l key val r) = Lean.RBNode.node color (Lean.RBNode.map f l) key (f key val) (Lean.RBNode.map f r)

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

Equations

• Lean.RBNode.toArray n = Lean.RBNode.fold (fun (acc : Array (Sigma β)) (k : α) (v : β k) => Array.push acc { fst := k, snd := v }) ∅ n

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

Equations

• Lean.RBNode.instEmptyCollectionRBNode = { emptyCollection := Lean.RBNode.leaf }

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

Equations

• Lean.RBMap α β cmp = { t : Lean.RBNode α fun (x : α) => β // Lean.RBNode.WellFormed cmp t }

Instances For

• Lake.instCoeDRBMapRBMap
• Lake.instCoeRBMapNameQuickCmpNameMap
• Lean.RBMap.instForInRBMapProd
• Lean.RBMap.instReprRBMap
• Lean.instEmptyCollectionRBMap
• Lean.instFromJsonRBMapString
• Lean.instInhabitedRBMap
• Lean.instToJsonRBMapString

@[inline]

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

Equations

• Lean.mkRBMap α β cmp = { val := Lean.RBNode.leaf, property := ⋯ }

@[inline]

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

Equations

• Lean.RBMap.empty = Lean.mkRBMap α β cmp

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

Equations

• Lean.instEmptyCollectionRBMap α β cmp = { emptyCollection := Lean.RBMap.empty }

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

Equations

• Lean.instInhabitedRBMap α β cmp = { default := ∅ }

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

Equations

• Lean.RBMap.depth f t = Lean.RBNode.depth f t.val

@[inline]

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

Equations

• Lean.RBMap.fold f x✝ x = match x✝, x with | b, { val := t, property := property } => Lean.RBNode.fold f b t

@[inline]

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

Equations

• Lean.RBMap.revFold f x✝ x = match x✝, x with | b, { val := t, property := property } => Lean.RBNode.revFold f b t

@[inline]

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

Equations

• Lean.RBMap.foldM f x✝ x = match x✝, x with | b, { val := t, property := property } => Lean.RBNode.foldM f b t

@[inline]

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

Equations

• Lean.RBMap.forM f t = Lean.RBMap.foldM (fun (x : PUnit) (k : α) (v : β) => f k v) PUnit.unit t

@[inline]

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

Equations

• Lean.RBMap.forIn t init f = Lean.RBNode.forIn t.val init fun (a : α) (b : β) (acc : σ) => f (a, b) acc

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

Equations

• Lean.RBMap.instForInRBMapProd = { forIn := fun {β_1 : Type u_1} [Monad m] => Lean.RBMap.forIn }

@[inline]

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

Equations

• Lean.RBMap.isEmpty x = match x with | { val := Lean.RBNode.leaf, property := property } => true | x => false

@[specialize #[]]

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

Equations

• Lean.RBMap.toList x = match x with | { val := t, property := property } => Lean.RBNode.revFold (fun (ps : List (α × β)) (k : α) (v : β) => (k, v) :: ps) [] t

@[inline]

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

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

Equations

• Lean.RBMap.min x = match x with | { val := t, property := property } => match Lean.RBNode.min t with | some { fst := k, snd := v } => some (k, v) | none => none

@[inline]

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

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

Equations

• Lean.RBMap.max x = match x with | { val := t, property := property } => match Lean.RBNode.max t with | some { fst := k, snd := v } => some (k, v) | none => none

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

Equations

• Lean.RBMap.instReprRBMap = { reprPrec := fun (m : Lean.RBMap α β cmp) (prec : Nat) => Repr.addAppParen (Std.Format.text "Lean.rbmapOf " ++ repr (Lean.RBMap.toList m)) prec }

@[inline]

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

Equations

• Lean.RBMap.insert x✝¹ x✝ x = match x✝¹, x✝, x with | { val := t, property := w }, k, v => { val := Lean.RBNode.insert cmp t k v, property := ⋯ }

@[inline]

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

Equations

• Lean.RBMap.erase x✝ x = match x✝, x with | { val := t, property := w }, k => { val := Lean.RBNode.erase cmp k t, property := ⋯ }

@[specialize #[]]

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

Equations

• Lean.RBMap.ofList [] = Lean.mkRBMap α β cmp
• Lean.RBMap.ofList ((k, v) :: xs) = Lean.RBMap.insert (Lean.RBMap.ofList xs) k v

@[inline]

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

Equations

• Lean.RBMap.findCore? x✝ x = match x✝, x with | { val := t, property := property }, x => Lean.RBNode.findCore cmp t x

@[inline]

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

Equations

• Lean.RBMap.find? x✝ x = match x✝, x with | { val := t, property := property }, x => Lean.RBNode.find cmp t x

@[inline]

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

Equations

• Lean.RBMap.findD t k v₀ = Option.getD (Lean.RBMap.find? t k) v₀

@[inline]

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

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

Equations

• Lean.RBMap.lowerBound x✝ x = match x✝, x with | { val := t, property := property }, x => Lean.RBNode.lowerBound cmp t x none

@[inline]

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

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

Equations

• Lean.RBMap.contains t a = Option.isSome (Lean.RBMap.find? t a)

@[inline]

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

Equations

• Lean.RBMap.fromList l cmp = List.foldl (fun (r : Lean.RBMap α β cmp) (p : α × β) => Lean.RBMap.insert r p.fst p.snd) (Lean.mkRBMap α β cmp) l

@[inline]

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

Equations

• Lean.RBMap.fromArray l cmp = Array.foldl (fun (r : Lean.RBMap α β cmp) (p : α × β) => Lean.RBMap.insert r p.fst p.snd) (Lean.mkRBMap α β cmp) l 0

@[inline]

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

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

Equations

• Lean.RBMap.all x✝ x = match x✝, x with | { val := t, property := property }, p => Lean.RBNode.all p t

@[inline]

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

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

Equations

• Lean.RBMap.any x✝ x = match x✝, x with | { val := t, property := property }, p => Lean.RBNode.any p t

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

The number of items in the RBMap.

Equations

• Lean.RBMap.size m = Lean.RBMap.fold (fun (sz : Nat) (x : α) (x : β) => sz + 1) 0 m

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

Equations

• Lean.RBMap.maxDepth t = Lean.RBNode.depth Nat.max t.val

@[inline]

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

Equations

• Lean.RBMap.min! t = match Lean.RBMap.min t with | some p => p | none => panicWithPosWithDecl "Lean.Data.RBMap" "Lean.RBMap.min!" 366 14 "map is empty"

@[inline]

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

Equations

• Lean.RBMap.max! t = match Lean.RBMap.max t with | some p => p | none => panicWithPosWithDecl "Lean.Data.RBMap" "Lean.RBMap.max!" 371 14 "map is empty"

@[inline]

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

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

Equations

• One or more equations did not get rendered due to their size.

def Lean.RBMap.mergeBy {α : Type u} {β : Type v} {cmp : α → α → Ordering} (mergeFn : α → β → β → β) (t₁ : Lean.RBMap α β cmp) (t₂ : Lean.RBMap α β cmp) : Lean.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.

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.rbmapOf l cmp = Lean.RBMap.fromList l cmp