# 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.

**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

## Instances For

**Alias** of `Batteries.mkHashMap`

.

Make a new hash map with the specified capacity.

## Equations

## Instances For

**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 `concat`

operations on lists, making it
useful for append-heavy uses such as logging and pretty printing.

## Equations

## Instances For

**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.

## Instances For

**Alias** of `Batteries.TotalBLE`

.

`TotalBLE le`

asserts that `le`

has a total order, that is, `le a b ∨ le b a`

.

## Equations

## Instances For

**Alias** of `Batteries.OrientedCmp`

.

`OrientedCmp cmp`

asserts that `cmp`

is determined by the relation `cmp x y = .lt`

.

## Equations

## Instances For

**Alias** of `Batteries.TransCmp`

.

`TransCmp cmp`

asserts that `cmp`

induces a transitive relation.

## Equations

## Instances For

**Alias** of `Batteries.BEqCmp`

.

`BEqCmp cmp`

asserts that `cmp x y = .eq`

and `x == y`

coincide.

## Equations

## Instances For

**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

## Instances For

**Alias** of `Batteries.OrientedOrd`

.

`OrientedOrd α`

asserts that the `Ord`

instance satisfies `OrientedCmp`

.

## Equations

## Instances For

**Alias** of `Batteries.TransOrd`

.

`TransOrd α`

asserts that the `Ord`

instance satisfies `TransCmp`

.

## Equations

## Instances For

**Alias** of `Batteries.BEqOrd`

.

`BEqOrd α`

asserts that the `Ord`

and `BEq`

instances are coherent via `BEqCmp`

.

## Equations

## Instances For

**Alias** of `Batteries.LawfulOrd`

.

`LawfulOrd α`

asserts that the `Ord`

instance satisfies `LawfulCmp`

.

## Equations

## Instances For

**Alias** of `Batteries.compareOfLessAndEq_eq_lt`

.

**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

## Instances For

**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

## Instances For

**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

## Instances For

**Alias** of `Batteries.mkRBSet`

.

`O(1)`

. Construct a new empty tree.

## Equations

## Instances For

**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

## Instances For

**Alias** of `Batteries.mkRBMap`

.

`O(1)`

. Construct a new empty map.

## Equations

## Instances For

**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

## Instances For

**Alias** of `Batteries.mkBinomialHeap`

.

`O(1)`

. Make a new empty binomial heap.

## Equations

## Instances For

**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.