Alter

📁 Source: Batteries/Data/RBMap/Alter.lean

Statistics

Metric	Count
Definitions alter, adapt, modify, OnRoot, Balanced, Ordered, RootOrdered, Zoomed, fill'	9
Theorems alter, modify, zoom, alter, modify, zoom, zoom', del, fill, ins, insertNew, del, fill, ins, insertNew, toRootOrdered, zoom_fill, zoom_fill', zoom_zoomed₂, alter, modify, RootOrdered_congr, find?_eq_zoom, modify_eq_alter, of_eq	25
Total	34

Batteries.RBMap

Definitions

Name	Category	Theorems
alter 📖	CompOp	—
modify 📖	CompOp	—

Batteries.RBMap.alter

Definitions

Name	Category	Theorems
adapt 📖	CompOp	—

Batteries.RBNode

Definitions

Name	Category	Theorems
OnRoot 📖	MathDef	1 math math: Path.zoom_zoomed₁

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
find?_eq_zoom 📖	mathematical	—	find? root? Batteries.RBNode Path zoom	—	find?.eq_def zoom.eq_def
modify_eq_alter 📖	mathematical	—	modify alter	—	—

Batteries.RBNode.Balanced

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
alter 📖	mathematical	Batteries.RBNode.Balanced	Batteries.RBNode.alter	—	zoom Batteries.RBNode.Path.Balanced.insertNew Batteries.RBNode.Path.Balanced.del Batteries.RBNode.RedRed.of_false append Batteries.RBNode.RedRed.imp Batteries.RBNode.Path.Balanced.fill
modify 📖	mathematical	Batteries.RBNode.Balanced	Batteries.RBNode.modify	—	alter Batteries.RBNode.modify_eq_alter
zoom 📖	—	Batteries.RBNode.Balanced Batteries.RBNode.Path.Balanced Batteries.RBNode.zoom Batteries.RBNode Batteries.RBNode.Path	—	—	Batteries.RBNode.zoom.eq_def

Batteries.RBNode.Ordered

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
alter 📖	mathematical	Batteries.RBNode.Path.RootOrdered Batteries.RBNode.OnRoot Batteries.RBNode.cmpEq Batteries.RBNode.Ordered	Batteries.RBNode.alter	—	zoom Batteries.RBNode.Path.Ordered.insertNew Batteries.RBNode.Path.Ordered.del append Batteries.RBNode.All.append Batteries.RBNode.Path.Ordered.fill Batteries.RBNode.All.imp Batteries.RBNode.cmpEq.lt_congr_right Batteries.RBNode.cmpEq.lt_congr_left
modify 📖	mathematical	Batteries.RBNode.OnRoot Batteries.RBNode.cmpEq Batteries.RBNode Batteries.RBNode.Path Batteries.RBNode.zoom Batteries.RBNode.Path.root Batteries.RBNode.Ordered	Batteries.RBNode.modify	—	alter Batteries.RBNode.cmpEq.RootOrdered_congr zoom Batteries.RBNode.modify_eq_alter
zoom 📖	mathematical	Batteries.RBNode.Ordered Batteries.RBNode.zoom Batteries.RBNode.Path.root Batteries.RBNode Batteries.RBNode.Path	Batteries.RBNode.Path.Ordered Batteries.RBNode.All Batteries.RBNode.Path.RootOrdered Batteries.RBNode.Path.Zoomed	—	zoom' Batteries.RBNode.All.trivial
zoom' 📖	—	Batteries.RBNode.Ordered Batteries.RBNode.Path.Ordered Batteries.RBNode.All Batteries.RBNode.Path.RootOrdered Batteries.RBNode.Path.Zoomed Batteries.RBNode.zoom Batteries.RBNode Batteries.RBNode.Path	—	—	Batteries.RBNode.Path.Ordered.fill Batteries.RBNode.Path.zoom_fill Batteries.RBNode.Path.zoom_zoomed₂

Batteries.RBNode.Path

Definitions

Name	Category	Theorems
Balanced 📖	CompData	—
Ordered 📖	MathDef	3 math math: Ordered.fill, ordered_iff, Batteries.RBNode.Ordered.zoom
RootOrdered 📖	MathDef	5 math math: Zoomed.toRootOrdered, Ordered.fill, rootOrdered_iff, Batteries.RBNode.Ordered.zoom, Batteries.RBNode.cmpEq.RootOrdered_congr
Zoomed 📖	MathDef	1 math math: Batteries.RBNode.Ordered.zoom
fill' 📖	CompOp	1 math math: zoom_fill'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
zoom_fill 📖	mathematical	Batteries.RBNode.zoom Batteries.RBNode Batteries.RBNode.Path	fill	—	zoom_fill'
zoom_fill' 📖	mathematical	—	fill' Batteries.RBNode.zoom fill	—	Batteries.RBNode.zoom.eq_def
zoom_zoomed₂ 📖	—	Batteries.RBNode.zoom Batteries.RBNode Batteries.RBNode.Path Zoomed	—	—	Batteries.RBNode.zoom.eq_def

Batteries.RBNode.Path.Balanced

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
del 📖	mathematical	Batteries.RBNode.Path.Balanced Batteries.RBNode.DelProp	Batteries.RBNode.Balanced Batteries.RBNode.Path.del Batteries.RBColor.black	—	Batteries.RBNode.Balanced.setBlack Batteries.RBNode.RedRed.setBlack Batteries.RBNode.RedRed.of_false Batteries.RBNode.Balanced.balLeft Batteries.RBNode.Balanced.balRight Batteries.RBNode.RedRed.imp
fill 📖	mathematical	Batteries.RBNode.Path.Balanced Batteries.RBNode.Balanced	Batteries.RBNode.Path.fill	—	—
ins 📖	mathematical	Batteries.RBNode.Path.Balanced Batteries.RBNode.RedRed Batteries.RBColor Batteries.RBColor.red	Batteries.RBNode.Balanced Batteries.RBNode.Path.ins Batteries.RBColor.black	—	Batteries.RBNode.RedRed.setBlack Batteries.RBNode.RedRed.balance1 Batteries.RBNode.RedRed.balance2
insertNew 📖	mathematical	Batteries.RBNode.Path.Balanced Batteries.RBColor.black	Batteries.RBNode.Balanced Batteries.RBNode.Path.insertNew	—	ins

Batteries.RBNode.Path.Ordered

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
del 📖	mathematical	Batteries.RBNode.Ordered Batteries.RBNode.Path.Ordered Batteries.RBNode.All Batteries.RBNode.Path.RootOrdered	Batteries.RBNode.Path.del	—	Batteries.RBNode.Ordered.setBlack Batteries.RBNode.Path.del.eq_def Batteries.RBNode.All_and Batteries.RBNode.Ordered.balLeft Batteries.RBNode.All.balLeft Batteries.RBNode.Ordered.balRight Batteries.RBNode.All.balRight
fill 📖	mathematical	—	Batteries.RBNode.Ordered Batteries.RBNode.Path.fill Batteries.RBNode.Path.Ordered Batteries.RBNode.All Batteries.RBNode.Path.RootOrdered	—	Batteries.RBNode.All.trivial
ins 📖	mathematical	Batteries.RBNode.Ordered Batteries.RBNode.Path.Ordered Batteries.RBNode.All Batteries.RBNode.Path.RootOrdered	Batteries.RBNode.Path.ins	—	Batteries.RBNode.Ordered.setBlack Batteries.RBNode.Path.ins.eq_def Batteries.RBNode.All_and Batteries.RBNode.Ordered.balance1 Batteries.RBNode.balance1_All Batteries.RBNode.Ordered.balance2 Batteries.RBNode.balance2_All
insertNew 📖	mathematical	Batteries.RBNode.Path.Ordered Batteries.RBNode.Path.RootOrdered	Batteries.RBNode.Ordered Batteries.RBNode.Path.insertNew	—	ins

Batteries.RBNode.Path.Zoomed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toRootOrdered 📖	mathematical	Batteries.RBNode.Path.Zoomed	Batteries.RBNode.Path.RootOrdered	—	—

Batteries.RBNode.WF

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
alter 📖	mathematical	Batteries.RBNode.Path.RootOrdered Batteries.RBNode.OnRoot Batteries.RBNode.cmpEq Batteries.RBNode.WF	Batteries.RBNode.alter	—	out Batteries.RBNode.WF_iff Batteries.RBNode.Ordered.alter Batteries.RBNode.Balanced.alter
modify 📖	mathematical	Batteries.RBNode.OnRoot Batteries.RBNode.cmpEq Batteries.RBNode Batteries.RBNode.Path Batteries.RBNode.zoom Batteries.RBNode.Path.root Batteries.RBNode.WF	Batteries.RBNode.modify	—	out Batteries.RBNode.WF_iff Batteries.RBNode.Ordered.modify Batteries.RBNode.Balanced.modify

Batteries.RBNode.cmpEq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
RootOrdered_congr 📖	mathematical	—	Batteries.RBNode.Path.RootOrdered	—	lt_congr_left lt_congr_right

Batteries.RBSet.ModifyWF

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_eq 📖	mathematical	Batteries.RBNode.cmpEq	Batteries.RBSet.ModifyWF	—	Batteries.RBNode.WF.modify Batteries.RBNode.find?_eq_zoom

---

← Back to Index