We set up deprecations for identifiers formerly in the Std namespace.

Note that we have not moved anything in the Std.CodeAction or Std.Linter namespace.

These deprecations do not cover Std.Tactic, the contents of which has been moved, but it would be much harder to generate the deprecations. Let's hope that people using the tactic implementations can work this out themselves.

@[deprecated Batteries.AssocList]

def Std.AssocList (α : Type u) (β : Type v) : Type (max u v)

Alias of Batteries.AssocList.

---

AssocList α β is "the same as" List (α × β), but flattening the structure leads to one fewer pointer indirection (in the current code generator). It is mainly intended as a component of HashMap, but it can also be used as a plain key-value map.

Equations

• Std.AssocList = Batteries.AssocList

@[deprecated Batteries.mkHashMap]

def Std.mkHashMap {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] (capacity : optParam Nat 0) : Batteries.HashMap α β

Alias of Batteries.mkHashMap.

---

Make a new hash map with the specified capacity.

Equations

• @Std.mkHashMap = @Batteries.mkHashMap

@[deprecated Batteries.DList]

def Std.DList (α : Type u) : Type u

Alias of Batteries.DList.

---

A difference List is a Function that, given a List, returns the original contents of the difference List prepended to the given List. This structure supports O(1) append and push operations on lists, making it useful for append-heavy uses such as logging and pretty printing.

Equations

• Std.DList = Batteries.DList

@[deprecated Batteries.PairingHeapImp.Heap]

def Std.PairingHeapImp.Heap (α : Type u) : Type u

Alias of Batteries.PairingHeapImp.Heap.

---

A Heap is the nodes of the pairing heap. Each node have two pointers: child going to the first child of this node, and sibling goes to the next sibling of this tree. So it actually encodes a forest where each node has children node.child, node.child.sibling, node.child.sibling.sibling, etc.

Each edge in this forest denotes a le a b relation that has been checked, so the root is smaller than everything else under it.

Equations

• Std.PairingHeapImp.Heap = Batteries.PairingHeapImp.Heap

@[deprecated Batteries.TotalBLE]

def Std.TotalBLE {α : Sort u_1} (le : α → α → Bool) : Prop

Alias of Batteries.TotalBLE.

---

TotalBLE le asserts that le has a total order, that is, le a b ∨ le b a.

Equations

• @Std.TotalBLE = @Batteries.TotalBLE

@[deprecated Batteries.OrientedCmp]

def Std.OrientedCmp {α : Sort u_1} (cmp : α → α → Ordering) : Prop

Alias of Batteries.OrientedCmp.

---

OrientedCmp cmp asserts that cmp is determined by the relation cmp x y = .lt.

Equations

• @Std.OrientedCmp = @Batteries.OrientedCmp

@[deprecated Batteries.TransCmp]

def Std.TransCmp {α : Sort u_1} (cmp : α → α → Ordering) : Prop

Alias of Batteries.TransCmp.

---

TransCmp cmp asserts that cmp induces a transitive relation.

Equations

• @Std.TransCmp = @Batteries.TransCmp

@[deprecated Batteries.BEqCmp]

def Std.BEqCmp {α : Type u_1} [BEq α] (cmp : α → α → Ordering) : Prop

Alias of Batteries.BEqCmp.

---

BEqCmp cmp asserts that cmp x y = .eq and x == y coincide.

Equations

• @Std.BEqCmp = @Batteries.BEqCmp

@[deprecated Batteries.LTCmp]

def Std.LTCmp {α : Type u_1} [LT α] (cmp : α → α → Ordering) : Prop

Alias of Batteries.LTCmp.

---

LTCmp cmp asserts that cmp x y = .lt and x < y coincide.

Equations

• @Std.LTCmp = @Batteries.LTCmp

@[deprecated Batteries.LECmp]

def Std.LECmp {α : Type u_1} [LE α] (cmp : α → α → Ordering) : Prop

Alias of Batteries.LECmp.

---

LECmp cmp asserts that cmp x y ≠ .gt and x ≤ y coincide.

Equations

• @Std.LECmp = @Batteries.LECmp

@[deprecated Batteries.LawfulCmp]

def Std.LawfulCmp {α : Type u_1} [LE α] [LT α] [BEq α] (cmp : α → α → Ordering) : Prop

Alias of Batteries.LawfulCmp.

---

LawfulCmp cmp asserts that the LE, LT, BEq instances are all coherent with each other and with cmp, describing a strict weak order (a linear order except for antisymmetry).

Equations

• @Std.LawfulCmp = @Batteries.LawfulCmp

@[deprecated Batteries.OrientedOrd]

def Std.OrientedOrd (α : Type u_1) [Ord α] : Prop

Alias of Batteries.OrientedOrd.

---

OrientedOrd α asserts that the Ord instance satisfies OrientedCmp.

Equations

• Std.OrientedOrd = Batteries.OrientedOrd

@[deprecated Batteries.TransOrd]

def Std.TransOrd (α : Type u_1) [Ord α] : Prop

Alias of Batteries.TransOrd.

---

TransOrd α asserts that the Ord instance satisfies TransCmp.

Equations

• Std.TransOrd = Batteries.TransOrd

@[deprecated Batteries.BEqOrd]

def Std.BEqOrd (α : Type u_1) [BEq α] [Ord α] : Prop

Alias of Batteries.BEqOrd.

---

BEqOrd α asserts that the Ord and BEq instances are coherent via BEqCmp.

Equations

• Std.BEqOrd = Batteries.BEqOrd

@[deprecated Batteries.LTOrd]

def Std.LTOrd (α : Type u_1) [LT α] [Ord α] : Prop

Alias of Batteries.LTOrd.

---

LTOrd α asserts that the Ord instance satisfies LTCmp.

Equations

• Std.LTOrd = Batteries.LTOrd

@[deprecated Batteries.LEOrd]

def Std.LEOrd (α : Type u_1) [LE α] [Ord α] : Prop

Alias of Batteries.LEOrd.

---

LEOrd α asserts that the Ord instance satisfies LECmp.

Equations

• Std.LEOrd = Batteries.LEOrd

@[deprecated Batteries.LawfulOrd]

def Std.LawfulOrd (α : Type u_1) [LE α] [LT α] [BEq α] [Ord α] : Prop

Alias of Batteries.LawfulOrd.

---

LawfulOrd α asserts that the Ord instance satisfies LawfulCmp.

Equations

• Std.LawfulOrd = Batteries.LawfulOrd

@[deprecated Batteries.compareOfLessAndEq_eq_lt]

theorem Std.compareOfLessAndEq_eq_lt {α : Type u_1} {x : α} {y : α} [LT α] [Decidable (x < y)] [DecidableEq α] : compareOfLessAndEq x y = Ordering.lt ↔ x < y

Alias of Batteries.compareOfLessAndEq_eq_lt.

@[deprecated Batteries.RBColor]

def Std.RBColor : Type

Alias of Batteries.RBColor.

---

In a red-black tree, every node has a color which is either "red" or "black" (this particular choice of colors is conventional). A nil node is considered black.

Equations

• Std.RBColor = Batteries.RBColor

@[deprecated Batteries.RBNode]

def Std.RBNode (α : Type u) : Type u

Alias of Batteries.RBNode.

---

A red-black tree. (This is an internal implementation detail of the RBSet type, which includes the invariants of the tree.) This is a binary search tree augmented with a "color" field which is either red or black for each node and used to implement the re-balancing operations. See: Red–black tree

Equations

• Std.RBNode = Batteries.RBNode

@[deprecated Batteries.RBSet]

def Std.RBSet (α : Type u) (cmp : α → α → Ordering) : Type u

Alias of Batteries.RBSet.

---

An RBSet is a self-balancing binary search tree. The cmp function is the comparator that will be used for performing searches; it should satisfy the requirements of TransCmp for it to have sensible behavior.

Equations

• Std.RBSet = Batteries.RBSet

@[deprecated Batteries.mkRBSet]

def Std.mkRBSet (α : Type u) (cmp : α → α → Ordering) : Batteries.RBSet α cmp

Alias of Batteries.mkRBSet.

---

O(1). Construct a new empty tree.

Equations

• Std.mkRBSet = Batteries.mkRBSet

@[deprecated Batteries.RBMap]

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

Alias of Batteries.RBMap.

---

An RBMap is a self-balancing binary search tree, used to store a key-value map. The cmp function is the comparator that will be used for performing searches; it should satisfy the requirements of TransCmp for it to have sensible behavior.

Equations

• Std.RBMap = Batteries.RBMap

@[deprecated Batteries.mkRBMap]

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

Alias of Batteries.mkRBMap.

---

O(1). Construct a new empty map.

Equations

• Std.mkRBMap = Batteries.mkRBMap

@[deprecated Batteries.BinomialHeap]

def Std.BinomialHeap (α : Type u) (le : α → α → Bool) : Type (max 0 u)

Alias of Batteries.BinomialHeap.

---

A binomial heap is a data structure which supports the following primary operations:

• insert : α → BinomialHeap α → BinomialHeap α: add an element to the heap
• deleteMin : BinomialHeap α → Option (α × BinomialHeap α): remove the minimum element from the heap
• merge : BinomialHeap α → BinomialHeap α → BinomialHeap α: combine two heaps

The first two operations are known as a "priority queue", so this could be called a "mergeable priority queue". The standard choice for a priority queue is a binary heap, which supports insert and deleteMin in O(log n), but merge is O(n). With a BinomialHeap, all three operations are O(log n).

Equations

• Std.BinomialHeap = Batteries.BinomialHeap

@[deprecated Batteries.mkBinomialHeap]

def Std.mkBinomialHeap (α : Type u) (le : α → α → Bool) : Batteries.BinomialHeap α le

Alias of Batteries.mkBinomialHeap.

---

O(1). Make a new empty binomial heap.

Equations

• Std.mkBinomialHeap = Batteries.mkBinomialHeap

@[deprecated Batteries.UFNode]

def Std.UFNode : Type

Alias of Batteries.UFNode.

---

Union-find node type

Equations

• Std.UFNode = Batteries.UFNode

@[deprecated Batteries.UnionFind]

def Std.UnionFind : Type

Alias of Batteries.UnionFind.

---

Union-find data structure

The UnionFind structure is an implementation of disjoint-set data structure that uses path compression to make the primary operations run in amortized nearly linear time. The nodes of a UnionFind structure s are natural numbers smaller than s.size. The structure associates with a canonical representative from its equivalence class. The structure can be extended using the push operation and equivalence classes can be updated using the union operation.

The main operations for UnionFind are:

• empty/mkEmpty are used to create a new empty structure.
• size returns the size of the data structure.
• push adds a new node to a structure, unlinked to any other node.
• union links two nodes of the data structure, joining their equivalence classes, and performs path compression.
• find returns the canonical representative of a node and updates the data structure using path compression.
• root returns the canonical representative of a node without altering the data structure.
• checkEquiv checks whether two nodes have the same canonical representative and updates the structure using path compression.

Most use cases should prefer find over root to benefit from the speedup from path-compression.

The main operations use Fin s.size to represent nodes of the union-find structure. Some alternatives are provided:

• unionN, findN, rootN, checkEquivN use Fin n with a proof that n = s.size.
• union!, find!, root!, checkEquiv! use Nat and panic when the indices are out of bounds.
• findD, rootD, checkEquivD use Nat and treat out of bound indices as isolated nodes.

The noncomputable relation UnionFind.Equiv is provided to use the equivalence relation from a UnionFind structure in the context of proofs.

Equations

• Std.UnionFind = Batteries.UnionFind