doc(data/vector3): improve wording (#14610)

leanprover-community · Jun 9, 2022 · 6826bf0 · 6826bf0
1 parent ab64f63
commit 6826bf0
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/src/data/vector3.lean b/src/data/vector3.lean
@@ -9,10 +9,10 @@ import tactic.localized
 /-!
 # Alternate definition of `vector` in terms of `fin2`
 
-This file provides a locale `vector3` which overrides `[a, b, c]` notation to create `vector3` not
-`list`.
+This file provides a locale `vector3` which overrides the `[a, b, c]` notation to create a `vector3`
+instead of a `list`.
 
-The `::` notation is overloaded by this file to mean `vector3.cons`.
+The `::` notation is also overloaded by this file to mean `vector3.cons`.
 -/
 
 open fin2 nat