Documentation

Mathlib.Data.Vector.Defs

The type Vector represents lists with fixed length.

def Mathlib.Vector (α : Type u) (n : ) :

Vector α n is the type of lists of length n with elements of type α.

Equations
Instances For
    Equations
    @[match_pattern]

    The empty vector with elements of type α

    Equations
    • Mathlib.Vector.nil = [],
    Instances For
      @[match_pattern]
      def Mathlib.Vector.cons {α : Type u} {n : } :
      αMathlib.Vector α nMathlib.Vector α n.succ

      If a : α and l : Vector α n, then cons a l, is the vector of length n + 1 whose first element is a and with l as the rest of the list.

      Equations
      Instances For
        @[reducible]
        def Mathlib.Vector.length {α : Type u} {n : } :

        The length of a vector.

        Equations
        • x.length = n
        Instances For
          def Mathlib.Vector.head {α : Type u} {n : } :
          Mathlib.Vector α n.succα

          The first element of a vector with length at least 1.

          Equations
          • x.head = match x with | a :: tail, property => a
          Instances For
            theorem Mathlib.Vector.head_cons {α : Type u} {n : } (a : α) (v : Mathlib.Vector α n) :
            (Mathlib.Vector.cons a v).head = a

            The head of a vector obtained by prepending is the element prepended.

            def Mathlib.Vector.tail {α : Type u} {n : } :
            Mathlib.Vector α nMathlib.Vector α (n - 1)

            The tail of a vector, with an empty vector having empty tail.

            Equations
            • x.tail = match x with | [], h => [], | head :: v, h => v,
            Instances For
              theorem Mathlib.Vector.tail_cons {α : Type u} {n : } (a : α) (v : Mathlib.Vector α n) :
              (Mathlib.Vector.cons a v).tail = v

              The tail of a vector obtained by prepending is the vector prepended. to

              @[simp]
              theorem Mathlib.Vector.cons_head_tail {α : Type u} {n : } (v : Mathlib.Vector α n.succ) :
              Mathlib.Vector.cons v.head v.tail = v

              Prepending the head of a vector to its tail gives the vector.

              def Mathlib.Vector.toList {α : Type u} {n : } (v : Mathlib.Vector α n) :
              List α

              The list obtained from a vector.

              Equations
              • v.toList = v
              Instances For
                def Mathlib.Vector.get {α : Type u} {n : } (l : Mathlib.Vector α n) (i : Fin n) :
                α

                nth element of a vector, indexed by a Fin type.

                Equations
                Instances For
                  def Mathlib.Vector.append {α : Type u} {n : } {m : } :
                  Mathlib.Vector α nMathlib.Vector α mMathlib.Vector α (n + m)

                  Appending a vector to another.

                  Equations
                  • x✝.append x = match x✝, x with | l₁, h₁, l₂, h₂ => l₁ ++ l₂,
                  Instances For
                    def Mathlib.Vector.elim {α : Type u_1} {C : {n : } → Mathlib.Vector α nSort u} (H : (l : List α) → C l, ) {n : } (v : Mathlib.Vector α n) :
                    C v

                    Elimination rule for Vector.

                    Equations
                    Instances For
                      def Mathlib.Vector.map {α : Type u} {β : Type v} {n : } (f : αβ) :

                      Map a vector under a function.

                      Equations
                      Instances For
                        @[simp]
                        theorem Mathlib.Vector.map_nil {α : Type u} {β : Type v} (f : αβ) :
                        Mathlib.Vector.map f Mathlib.Vector.nil = Mathlib.Vector.nil

                        A nil vector maps to a nil vector.

                        @[simp]
                        theorem Mathlib.Vector.map_cons {α : Type u} {β : Type v} {n : } (f : αβ) (a : α) (v : Mathlib.Vector α n) :

                        map is natural with respect to cons.

                        def Mathlib.Vector.map₂ {α : Type u} {β : Type v} {φ : Type w} {n : } (f : αβφ) :

                        Mapping two vectors under a curried function of two variables.

                        Equations
                        Instances For
                          def Mathlib.Vector.replicate {α : Type u} (n : ) (a : α) :

                          Vector obtained by repeating an element.

                          Equations
                          Instances For
                            def Mathlib.Vector.drop {α : Type u} {n : } (i : ) :
                            Mathlib.Vector α nMathlib.Vector α (n - i)

                            Drop i elements from a vector of length n; we can have i > n.

                            Equations
                            Instances For
                              def Mathlib.Vector.take {α : Type u} {n : } (i : ) :

                              Take i elements from a vector of length n; we can have i > n.

                              Equations
                              Instances For
                                def Mathlib.Vector.eraseIdx {α : Type u} {n : } (i : Fin n) :
                                Mathlib.Vector α nMathlib.Vector α (n - 1)

                                Remove the element at position i from a vector of length n.

                                Equations
                                Instances For
                                  @[deprecated Mathlib.Vector.eraseIdx]
                                  def Mathlib.Vector.removeNth {α : Type u} {n : } (i : Fin n) :
                                  Mathlib.Vector α nMathlib.Vector α (n - 1)

                                  Alias of Mathlib.Vector.eraseIdx.


                                  Remove the element at position i from a vector of length n.

                                  Equations
                                  Instances For
                                    def Mathlib.Vector.ofFn {α : Type u} {n : } :
                                    (Fin nα)Mathlib.Vector α n

                                    Vector of length n from a function on Fin n.

                                    Equations
                                    Instances For
                                      def Mathlib.Vector.congr {α : Type u} {n : } {m : } (h : n = m) :

                                      Create a vector from another with a provably equal length.

                                      Equations
                                      Instances For
                                        def Mathlib.Vector.mapAccumr {α : Type u} {β : Type v} {n : } {σ : Type} (f : ασσ × β) :
                                        Mathlib.Vector α nσσ × Mathlib.Vector β n

                                        Runs a function over a vector returning the intermediate results and a final result.

                                        Equations
                                        Instances For
                                          def Mathlib.Vector.mapAccumr₂ {n : } {α : Type} {β : Type} {σ : Type} {φ : Type} (f : αβσσ × φ) :
                                          Mathlib.Vector α nMathlib.Vector β nσσ × Mathlib.Vector φ n

                                          Runs a function over a pair of vectors returning the intermediate results and a final result.

                                          Equations
                                          Instances For

                                            Shift Primitives #

                                            def Mathlib.Vector.shiftLeftFill {α : Type u} {n : } (v : Mathlib.Vector α n) (i : ) (fill : α) :

                                            shiftLeftFill v i is the vector obtained by left-shifting v i times and padding with the fill argument. If v.length < i then this will return replicate n fill.

                                            Equations
                                            Instances For
                                              def Mathlib.Vector.shiftRightFill {α : Type u} {n : } (v : Mathlib.Vector α n) (i : ) (fill : α) :

                                              shiftRightFill v i is the vector obtained by right-shifting v i times and padding with the fill argument. If v.length < i then this will return replicate n fill.

                                              Equations
                                              Instances For

                                                Basic Theorems #

                                                theorem Mathlib.Vector.eq {α : Type u} {n : } (a1 : Mathlib.Vector α n) (a2 : Mathlib.Vector α n) :
                                                a1.toList = a2.toLista1 = a2

                                                Vector is determined by the underlying list.

                                                theorem Mathlib.Vector.eq_nil {α : Type u} (v : Mathlib.Vector α 0) :
                                                v = Mathlib.Vector.nil

                                                A vector of length 0 is a nil vector.

                                                @[simp]
                                                theorem Mathlib.Vector.toList_mk {α : Type u} {n : } (v : List α) (P : v.length = n) :

                                                Vector of length from a list v with witness that v has length n maps to v under toList.

                                                @[simp]
                                                theorem Mathlib.Vector.toList_nil {α : Type u} :
                                                Mathlib.Vector.nil.toList = []

                                                A nil vector maps to a nil list.

                                                @[simp]
                                                theorem Mathlib.Vector.toList_length {α : Type u} {n : } (v : Mathlib.Vector α n) :
                                                v.toList.length = n

                                                The length of the list to which a vector of length n maps is n.

                                                @[simp]
                                                theorem Mathlib.Vector.toList_cons {α : Type u} {n : } (a : α) (v : Mathlib.Vector α n) :
                                                (Mathlib.Vector.cons a v).toList = a :: v.toList

                                                toList of cons of a vector and an element is the cons of the list obtained by toList and the element

                                                @[simp]
                                                theorem Mathlib.Vector.toList_append {α : Type u} {n : } {m : } (v : Mathlib.Vector α n) (w : Mathlib.Vector α m) :
                                                (v.append w).toList = v.toList ++ w.toList

                                                Appending of vectors corresponds under toList to appending of lists.

                                                @[simp]
                                                theorem Mathlib.Vector.toList_drop {α : Type u} {n : } {m : } (v : Mathlib.Vector α m) :
                                                (Mathlib.Vector.drop n v).toList = List.drop n v.toList

                                                drop of vectors corresponds under toList to drop of lists.

                                                @[simp]
                                                theorem Mathlib.Vector.toList_take {α : Type u} {n : } {m : } (v : Mathlib.Vector α m) :
                                                (Mathlib.Vector.take n v).toList = List.take n v.toList

                                                take of vectors corresponds under toList to take of lists.

                                                instance Mathlib.Vector.instGetElemNatLt {α : Type u} {n : } :
                                                GetElem (Mathlib.Vector α n) α fun (x : Mathlib.Vector α n) (i : ) => i < n
                                                Equations
                                                • Mathlib.Vector.instGetElemNatLt = { getElem := fun (x : Mathlib.Vector α n) (i : ) (h : i < n) => x.get i, h }