Documentation

Mathlib.Data.Vector

The type Vector represents lists with fixed length.

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

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

Equations
Instances For
    instance Vector.instDecidableEqVector {α : Type u} {n : } [DecidableEq α] :
    Equations
    @[match_pattern]
    def Vector.nil {α : Type u} :
    Vector α 0

    The empty vector with elements of type α

    Equations
    Instances For
      @[match_pattern]
      def Vector.cons {α : Type u} {n : } :
      αVector α nVector α (Nat.succ n)

      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 Vector.length {α : Type u} {n : } :
        Vector α n

        The length of a vector.

        Equations
        Instances For
          def Vector.head {α : Type u} {n : } :
          Vector α (Nat.succ n)α

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

          Equations
          Instances For
            theorem Vector.head_cons {α : Type u} {n : } (a : α) (v : Vector α n) :

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

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

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

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              theorem Vector.tail_cons {α : Type u} {n : } (a : α) (v : Vector α n) :

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

              @[simp]
              theorem Vector.cons_head_tail {α : Type u} {n : } (v : Vector α (Nat.succ n)) :

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

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

              The list obtained from a vector.

              Equations
              Instances For
                def Vector.get {α : Type u} {n : } :
                Vector α nFin nα

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

                Equations
                Instances For
                  def Vector.append {α : Type u} {n : } {m : } :
                  Vector α nVector α mVector α (n + m)

                  Appending a vector to another.

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

                    Elimination rule for Vector.

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

                      Map a vector under a function.

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

                        A nil vector maps to a nil vector.

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

                        map is natural with respect to cons.

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

                        Mapping two vectors under a curried function of two variables.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          def Vector.replicate {α : Type u} (n : ) (a : α) :
                          Vector α n

                          Vector obtained by repeating an element.

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

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

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

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

                              Equations
                              Instances For
                                def Vector.removeNth {α : Type u} {n : } (i : Fin n) :
                                Vector α nVector α (n - 1)

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

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

                                  Vector of length n from a function on Fin n.

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

                                    Create a vector from another with a provably equal length.

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

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

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        def Vector.mapAccumr₂ {n : } {α : Type} {β : Type} {σ : Type} {φ : Type} (f : αβσσ × φ) :
                                        Vector α nVector β nσσ × Vector φ n

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

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For

                                          Shift Primitives #

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

                                          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 Vector.shiftRightFill {α : Type u} {n : } (v : Vector α n) (i : ) (fill : α) :
                                            Vector α n

                                            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 Vector.eq {α : Type u} {n : } (a1 : Vector α n) (a2 : Vector α n) :
                                              Vector.toList a1 = Vector.toList a2a1 = a2

                                              Vector is determined by the underlying list.

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

                                              A vector of length 0 is a nil vector.

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

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

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

                                              A nil vector maps to a nil list.

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

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

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

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

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

                                              Appending of vectors corresponds under toList to appending of lists.

                                              @[simp]
                                              theorem Vector.toList_drop {α : Type u} {n : } {m : } (v : Vector α m) :

                                              drop of vectors corresponds under toList to drop of lists.

                                              @[simp]
                                              theorem Vector.toList_take {α : Type u} {n : } {m : } (v : Vector α m) :

                                              take of vectors corresponds under toList to take of lists.

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