Documentation

Batteries.StdDeprecations

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
Instances For
    @[deprecated Batteries.mkHashMap]
    def Std.mkHashMap {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] (capacity : optParam Nat 0) :

    Alias of Batteries.mkHashMap.


    Make a new hash map with the specified capacity.

    Equations
    Instances For
      @[deprecated Batteries.DList]
      def Std.DList (α : 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
      Instances For
        @[deprecated Batteries.PairingHeapImp.Heap]

        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
        Instances For
          @[deprecated Batteries.TotalBLE]
          def Std.TotalBLE {α : Sort u_1} (le : ααBool) :

          Alias of Batteries.TotalBLE.


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

          Equations
          Instances For
            @[deprecated Batteries.OrientedCmp]
            def Std.OrientedCmp {α : Sort u_1} (cmp : ααOrdering) :

            Alias of Batteries.OrientedCmp.


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

            Equations
            Instances For
              @[deprecated Batteries.TransCmp]
              def Std.TransCmp {α : Sort u_1} (cmp : ααOrdering) :

              Alias of Batteries.TransCmp.


              TransCmp cmp asserts that cmp induces a transitive relation.

              Equations
              Instances For
                @[deprecated Batteries.BEqCmp]
                def Std.BEqCmp {α : Type u_1} [BEq α] (cmp : ααOrdering) :

                Alias of Batteries.BEqCmp.


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

                Equations
                Instances For
                  @[deprecated Batteries.LTCmp]
                  def Std.LTCmp {α : Type u_1} [LT α] (cmp : ααOrdering) :

                  Alias of Batteries.LTCmp.


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

                  Equations
                  Instances For
                    @[deprecated Batteries.LECmp]
                    def Std.LECmp {α : Type u_1} [LE α] (cmp : ααOrdering) :

                    Alias of Batteries.LECmp.


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

                    Equations
                    Instances For
                      @[deprecated Batteries.LawfulCmp]
                      def Std.LawfulCmp {α : Type u_1} [LE α] [LT α] [BEq α] (cmp : ααOrdering) :

                      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
                        @[deprecated Batteries.OrientedOrd]
                        def Std.OrientedOrd (α : Type u_1) [Ord α] :

                        Alias of Batteries.OrientedOrd.


                        OrientedOrd α asserts that the Ord instance satisfies OrientedCmp.

                        Equations
                        Instances For
                          @[deprecated Batteries.TransOrd]
                          def Std.TransOrd (α : Type u_1) [Ord α] :

                          Alias of Batteries.TransOrd.


                          TransOrd α asserts that the Ord instance satisfies TransCmp.

                          Equations
                          Instances For
                            @[deprecated Batteries.BEqOrd]
                            def Std.BEqOrd (α : Type u_1) [BEq α] [Ord α] :

                            Alias of Batteries.BEqOrd.


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

                            Equations
                            Instances For
                              @[deprecated Batteries.LTOrd]
                              def Std.LTOrd (α : Type u_1) [LT α] [Ord α] :

                              Alias of Batteries.LTOrd.


                              LTOrd α asserts that the Ord instance satisfies LTCmp.

                              Equations
                              Instances For
                                @[deprecated Batteries.LEOrd]
                                def Std.LEOrd (α : Type u_1) [LE α] [Ord α] :

                                Alias of Batteries.LEOrd.


                                LEOrd α asserts that the Ord instance satisfies LECmp.

                                Equations
                                Instances For
                                  @[deprecated Batteries.LawfulOrd]
                                  def Std.LawfulOrd (α : Type u_1) [LE α] [LT α] [BEq α] [Ord α] :

                                  Alias of Batteries.LawfulOrd.


                                  LawfulOrd α asserts that the Ord instance satisfies LawfulCmp.

                                  Equations
                                  Instances For
                                    @[deprecated Batteries.compareOfLessAndEq_eq_lt]
                                    theorem Std.compareOfLessAndEq_eq_lt {α : Type u_1} {x : α} {y : α} [LT α] [Decidable (x < y)] [DecidableEq α] :

                                    Alias of Batteries.compareOfLessAndEq_eq_lt.

                                    @[deprecated Batteries.RBColor]

                                    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
                                      @[deprecated Batteries.RBNode]
                                      def Std.RBNode (α : 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
                                      Instances For
                                        @[deprecated Batteries.RBSet]
                                        def Std.RBSet (α : Type u) (cmp : ααOrdering) :

                                        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
                                          @[deprecated Batteries.mkRBSet]
                                          def Std.mkRBSet (α : Type u) (cmp : ααOrdering) :

                                          Alias of Batteries.mkRBSet.


                                          O(1). Construct a new empty tree.

                                          Equations
                                          Instances For
                                            @[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
                                            Instances For
                                              @[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
                                              Instances For
                                                @[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:

                                                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
                                                  @[deprecated Batteries.mkBinomialHeap]
                                                  def Std.mkBinomialHeap (α : Type u) (le : ααBool) :

                                                  Alias of Batteries.mkBinomialHeap.


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

                                                  Equations
                                                  Instances For
                                                    @[deprecated Batteries.UFNode]

                                                    Alias of Batteries.UFNode.


                                                    Union-find node type

                                                    Equations
                                                    Instances For
                                                      @[deprecated Batteries.UnionFind]

                                                      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
                                                      Instances For