1 files changed, 10 insertions, 15 deletions
diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean
index a09d6ac2..c4c4d9f2 100644
--- a/backends/lean/Base/Primitives/Vec.lean
+++ b/backends/lean/Base/Primitives/Vec.lean
@@ -1,3 +1,4 @@
+/- Vectors -/
 import Lean
 import Lean.Meta.Tactic.Simp
 import Init.Data.List.Basic
@@ -5,6 +6,7 @@ import Mathlib.Tactic.RunCmd
 import Mathlib.Tactic.Linarith
 import Base.IList
 import Base.Primitives.Scalar
+import Base.Primitives.Array
 import Base.Arith
 import Base.Progress.Base
 
@@ -12,19 +14,16 @@ namespace Primitives
 
 open Result Error
 
--------------
--- VECTORS --
--------------
-
 def Vec (α : Type u) := { l : List α // l.length ≤ Usize.max }
 
--- TODO: do we really need it? It should be with Subtype by default
-instance Vec.cast (a : Type u): Coe (Vec a) (List a)  where coe := λ v => v.val
-
 instance (a : Type u) : Arith.HasIntProp (Vec a) where
   prop_ty := λ v => 0 ≤ v.val.len ∧ v.val.len ≤ Scalar.max ScalarTy.Usize
   prop := λ ⟨ _, l ⟩ => by simp[Scalar.max, List.len_eq_length, *]
 
+instance {α : Type u} (p : Vec α → Prop) : Arith.HasIntProp (Subtype p) where
+  prop_ty := λ x => p x
+  prop := λ x => x.property
+
 @[simp]
 abbrev Vec.length {α : Type u} (v : Vec α) : Int := v.val.len
 
@@ -80,7 +79,7 @@ theorem Vec.insert_spec {α : Type u} (v: Vec α) (i: Usize) (x: α)
   ∃ nv, v.insert α i x = ret nv ∧ nv.val = v.val.update i.val x := by
   simp [insert, *]
 
-def Vec.index (α : Type u) (v: Vec α) (i: Usize) : Result α :=
+def Vec.index_shared (α : Type u) (v: Vec α) (i: Usize) : Result α :=
   match v.val.indexOpt i.val with
   | none => fail .arrayOutOfBounds
   | some x => ret x
@@ -91,10 +90,10 @@ def Vec.index (α : Type u) (v: Vec α) (i: Usize) : Result α :=
  -/
 
 @[pspec]
-theorem Vec.index_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize)
+theorem Vec.index_shared_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize)
   (hbound : i.val < v.length) :
-  ∃ x, v.index α i = ret x ∧ x = v.val.index i.val := by
-  simp only [index]
+  ∃ x, v.index_shared α i = ret x ∧ x = v.val.index i.val := by
+  simp only [index_shared]
   -- TODO: dependent rewrite
   have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
   simp [*]
@@ -120,10 +119,6 @@ theorem Vec.index_mut_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize)
   have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
   simp [*]
 
-instance {α : Type u} (p : Vec α → Prop) : Arith.HasIntProp (Subtype p) where
-  prop_ty := λ x => p x
-  prop := λ x => x.property
-
 def Vec.index_mut_back (α : Type u) (v: Vec α) (i: Usize) (x: α) : Result (Vec α) :=
   match v.val.indexOpt i.val with
   | none => fail .arrayOutOfBounds