- leaf: {α : Type u} → {β : α → Type v} → Lean.RBNode α β
- node: {α : Type u} → {β : α → Type v} → Lean.RBColor → Lean.RBNode α β → (key : α) → β key → Lean.RBNode α β → Lean.RBNode α β
Instances For
Equations
- Lean.RBNode.depth f Lean.RBNode.leaf = 0
- Lean.RBNode.depth f (Lean.RBNode.node color l key val r) = (f (Lean.RBNode.depth f l) (Lean.RBNode.depth f r)).succ
Instances For
Equations
- Lean.RBNode.leaf.min = none
- (Lean.RBNode.node color Lean.RBNode.leaf k v rchild).min = some ⟨k, v⟩
- (Lean.RBNode.node color l key val rchild).min = l.min
Instances For
Equations
- Lean.RBNode.leaf.max = none
- (Lean.RBNode.node color lchild k v Lean.RBNode.leaf).max = some ⟨k, v⟩
- (Lean.RBNode.node color lchild key val r).max = r.max
Instances For
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
Instances For
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
Instances For
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
Instances For
Equations
- as.forIn 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
Instances For
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)
Instances For
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
Instances For
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)
Instances For
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)
Instances For
Equations
- Lean.RBNode.singleton k v = Lean.RBNode.node Lean.RBColor.red Lean.RBNode.leaf k v Lean.RBNode.leaf
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- x.isRed = match x with | Lean.RBNode.node Lean.RBColor.red lchild key val rchild => true | x => false
Instances For
Equations
- x.isBlack = match x with | Lean.RBNode.node Lean.RBColor.black lchild key val rchild => true | x => false
Instances For
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
Instances For
Equations
- x.setBlack = match x with | Lean.RBNode.node color l k v r => Lean.RBNode.node Lean.RBColor.black l k v r | e => e
Instances For
Equations
- Lean.RBNode.insert cmp t k v = if t.isRed = true then (Lean.RBNode.ins cmp t k v).setBlack else Lean.RBNode.ins cmp t k v
Instances For
Equations
- x.setRed = match x with | Lean.RBNode.node color a k v b => Lean.RBNode.node Lean.RBColor.red a k v b | e => e
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
The number of nodes in the tree.
Equations
- Lean.RBNode.leaf.size = 0
- (Lean.RBNode.node color l key val r).size = l.size + r.size + 1
Instances For
Instances For
Equations
- One or more equations did not get rendered due to their size.
- Lean.RBNode.del cmp x Lean.RBNode.leaf = Lean.RBNode.leaf
Instances For
Equations
- Lean.RBNode.erase cmp x t = let t := Lean.RBNode.del cmp x t; t.setBlack
Instances For
Equations
- One or more equations did not get rendered due to their size.
- Lean.RBNode.findCore cmp Lean.RBNode.leaf x = none
Instances For
Equations
- Lean.RBNode.find cmp Lean.RBNode.leaf x = none
- Lean.RBNode.find cmp (Lean.RBNode.node color a ky vy b) x = match cmp x ky with | Ordering.lt => Lean.RBNode.find cmp a x | Ordering.gt => Lean.RBNode.find cmp b x | Ordering.eq => some vy
Instances For
Equations
- One or more equations did not get rendered due to their size.
- Lean.RBNode.lowerBound cmp Lean.RBNode.leaf x✝ x = x
Instances For
- 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'
Instances For
Equations
- One or more equations did not get rendered due to their size.
- Lean.RBNode.mapM f Lean.RBNode.leaf = pure Lean.RBNode.leaf
Instances For
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)
Instances For
Equations
- n.toArray = Lean.RBNode.fold (fun (acc : Array (Sigma β)) (k : α) (v : β k) => acc.push ⟨k, v⟩) ∅ n
Instances For
Equations
- Lean.RBNode.instEmptyCollection = { emptyCollection := Lean.RBNode.leaf }
Equations
- Lean.RBMap α β cmp = { t : Lean.RBNode α fun (x : α) => β // Lean.RBNode.WellFormed cmp t }
Instances For
Equations
- Lean.instEmptyCollectionRBMap α β cmp = { emptyCollection := Lean.RBMap.empty }
Equations
- Lean.instInhabitedRBMap α β cmp = { default := ∅ }
Equations
- Lean.RBMap.depth f t = Lean.RBNode.depth f t.val
Instances For
Equations
- Lean.RBMap.fold f x✝ x = match x✝, x with | b, ⟨t, property⟩ => Lean.RBNode.fold f b t
Instances For
Equations
- Lean.RBMap.revFold f x✝ x = match x✝, x with | b, ⟨t, property⟩ => Lean.RBNode.revFold f b t
Instances For
Equations
- Lean.RBMap.foldM f x✝ x = match x✝, x with | b, ⟨t, property⟩ => Lean.RBNode.foldM f b t
Instances For
Equations
- Lean.RBMap.forM f t = Lean.RBMap.foldM (fun (x : PUnit) (k : α) (v : β) => f k v) PUnit.unit t
Instances For
Equations
- t.forIn init f = t.val.forIn init fun (a : α) (b : β) (acc : σ) => f (a, b) acc
Instances For
Instances For
Equations
- x.toList = match x with | ⟨t, property⟩ => Lean.RBNode.revFold (fun (ps : List (α × β)) (k : α) (v : β) => (k, v) :: ps) [] t
Instances For
Returns the kv pair (a,b)
such that a ≤ k
for all keys in the RBMap.
Equations
Instances For
Returns the kv pair (a,b)
such that a ≥ k
for all keys in the RBMap.
Equations
Instances For
Equations
- Lean.RBMap.instRepr = { reprPrec := fun (m : Lean.RBMap α β cmp) (prec : Nat) => Repr.addAppParen (Std.Format.text "Lean.rbmapOf " ++ repr m.toList) prec }
Equations
- x✝¹.insert x✝ x = match x✝¹, x✝, x with | ⟨t, w⟩, k, v => ⟨Lean.RBNode.insert cmp t k v, ⋯⟩
Instances For
Equations
- x✝.erase x = match x✝, x with | ⟨t, w⟩, k => ⟨Lean.RBNode.erase cmp k t, ⋯⟩
Instances For
Equations
- Lean.RBMap.ofList [] = Lean.mkRBMap α β cmp
- Lean.RBMap.ofList ((k, v) :: xs) = (Lean.RBMap.ofList xs).insert k v
Instances For
Equations
- x✝.findCore? x = match x✝, x with | ⟨t, property⟩, x => Lean.RBNode.findCore cmp t x
Instances For
Equations
- x✝.find? x = match x✝, x with | ⟨t, property⟩, x => Lean.RBNode.find cmp t x
Instances For
Equations
- t.findD k v₀ = (t.find? k).getD v₀
Instances For
(lowerBound k) retrieves the kv pair of the largest key smaller than or equal to k
,
if it exists.
Equations
- x✝.lowerBound x = match x✝, x with | ⟨t, property⟩, x => Lean.RBNode.lowerBound cmp t x none
Instances For
Returns true if the given key a
is in the RBMap.
Equations
- t.contains a = (t.find? a).isSome
Instances For
Equations
- Lean.RBMap.fromList l cmp = List.foldl (fun (r : Lean.RBMap α β cmp) (p : α × β) => r.insert p.fst p.snd) (Lean.mkRBMap α β cmp) l
Instances For
Equations
- Lean.RBMap.fromArray l cmp = Array.foldl (fun (r : Lean.RBMap α β cmp) (p : α × β) => r.insert p.fst p.snd) (Lean.mkRBMap α β cmp) l 0
Instances For
Returns true if the given predicate is true for all items in the RBMap.
Equations
- x✝.all x = match x✝, x with | ⟨t, property⟩, p => Lean.RBNode.all p t
Instances For
Returns true if the given predicate is true for any item in the RBMap.
Equations
- x✝.any x = match x✝, x with | ⟨t, property⟩, p => Lean.RBNode.any p t
Instances For
The number of items in the RBMap.
Equations
- m.size = Lean.RBMap.fold (fun (sz : Nat) (x : α) (x : β) => sz + 1) 0 m
Instances For
Equations
- t.maxDepth = Lean.RBNode.depth Nat.max t.val
Instances For
Equations
- t.min! = match t.min with | some p => p | none => panicWithPosWithDecl "Lean.Data.RBMap" "Lean.RBMap.min!" 366 14 "map is empty"
Instances For
Equations
- t.max! = match t.max with | some p => p | none => panicWithPosWithDecl "Lean.Data.RBMap" "Lean.RBMap.max!" 371 14 "map is empty"
Instances For
Attempts to find the value with key k : α
in t
and panics if there is no such key.
Equations
- t.find! k = match t.find? k with | some b => b | none => panicWithPosWithDecl "Lean.Data.RBMap" "Lean.RBMap.find!" 377 14 "key is not in the map"
Instances For
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.
Instances For
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.
Instances For
Equations
- Lean.rbmapOf l cmp = Lean.RBMap.fromList l cmp