Feat: Port/data.vector.basic (#1633)

Port of data.vector.basic

Does a realignment of `Vector` functions to mirror the `List` equivalents, particularly for `nth` which has been replaced by `get`

Mathlib.lean

@@ -463,6 +463,7 @@ import Mathlib.Data.UInt
 import Mathlib.Data.ULift
 import Mathlib.Data.UnionFind
 import Mathlib.Data.Vector
+import Mathlib.Data.Vector.Basic
 import Mathlib.Data.Zmod.AdHocDefs
 import Mathlib.Deprecated.Group
 import Mathlib.Deprecated.Ring

Mathlib/Data/Vector.lean

@@ -90,10 +90,11 @@ def toList (v : Vector α n) : List α :=
   v.1
 #align vector.to_list Vector.toList
 
+-- porting notes: align to `List` API
 /-- nth element of a vector, indexed by a `Fin` type. -/
-def nth : ∀ _ : Vector α n, Fin n → α
+def get : ∀ _ : Vector α n, Fin n → α
   | ⟨l, h⟩, i => l.nthLe i.1 (by rw [h] ; exact i.2)
-#align vector.nth Vector.nth
+#align vector.nth Vector.get
 
 /-- Appending a vector to another. -/
 def append {n m : Nat} : Vector α n → Vector α m → Vector α (n + m)
@@ -217,7 +218,7 @@ theorem toList_mk (v : List α) (P : List.length v = n) : toList (Subtype.mk v P
 #align vector.to_list_mk Vector.toList_mk
 
 /-- A nil vector maps to a nil list. -/
-@[simp]
+@[simp, nolint simpNF] -- Porting note: simp can prove this in the future
 theorem toList_nil : toList nil = @List.nil α :=
   rfl
 #align vector.to_list_nil Vector.toList_nil