3 files changed, 25 insertions, 26 deletions
diff --git a/backends/lean/Base/Primitives/Alloc.lean b/backends/lean/Base/Primitives/Alloc.lean
index 34590499..6c89c6bb 100644
--- a/backends/lean/Base/Primitives/Alloc.lean
+++ b/backends/lean/Base/Primitives/Alloc.lean
@@ -16,16 +16,16 @@ def deref_mut (T : Type) (x : T) : Result T := ret x
 def deref_mut_back (T : Type) (_ : T) (x : T) : Result T := ret x
 
 /-- Trait instance -/
-def coreOpsDerefInst (Self : Type) :
+def coreopsDerefInst (Self : Type) :
   core.ops.deref.Deref Self := {
   Target := Self
   deref := deref Self
 }
 
 /-- Trait instance -/
-def coreOpsDerefMutInst (Self : Type) :
+def coreopsDerefMutInst (Self : Type) :
   core.ops.deref.DerefMut Self := {
-  derefInst := coreOpsDerefInst Self
+  derefInst := coreopsDerefInst Self
   deref_mut := deref_mut Self
   deref_mut_back := deref_mut_back Self
 }
diff --git a/backends/lean/Base/Primitives/ArraySlice.lean b/backends/lean/Base/Primitives/ArraySlice.lean
index cfc9a6b2..8bb9a855 100644
--- a/backends/lean/Base/Primitives/ArraySlice.lean
+++ b/backends/lean/Base/Primitives/ArraySlice.lean
@@ -439,23 +439,14 @@ def core.array.Array.index_mut_back
   (a : Array T N) (i : I) (x : inst.indexInst.Output) : Result (Array T N) :=
   sorry -- TODO
 
-/- Trait implementation: [core::slice::index::[T]] -/
-def core.slice.index.Slice.coreopsindexIndexInst (T I : Type)
-  (inst : core.slice.index.SliceIndex I (Slice T)) :
-  core.ops.index.Index (Slice T) I := {
-  Output := inst.Output
-  index := core.slice.index.Slice.index T I inst
-}
-
 /- Trait implementation: [core::slice::index::private_slice_index::Range] -/
-def core.slice.index.private_slice_index.Range.coresliceindexprivate_slice_indexSealedInst
+def core.slice.index.private_slice_index.SealedRangeUsizeInst
   : core.slice.index.private_slice_index.Sealed (Range Usize) := {}
 
 /- Trait implementation: [core::slice::index::Range] -/
-def core.slice.index.Range.coresliceindexSliceIndexInst (T : Type) :
+def core.slice.index.SliceIndexRangeUsizeSliceTInst (T : Type) :
   core.slice.index.SliceIndex (Range Usize) (Slice T) := {
-  sealedInst :=
-    core.slice.index.private_slice_index.Range.coresliceindexprivate_slice_indexSealedInst
+  sealedInst := core.slice.index.private_slice_index.SealedRangeUsizeInst
   Output := Slice T
   get := core.slice.index.Range.get T
   get_mut := core.slice.index.Range.get_mut T
@@ -468,16 +459,24 @@ def core.slice.index.Range.coresliceindexSliceIndexInst (T : Type) :
 }
 
 /- Trait implementation: [core::slice::index::[T]] -/
-def core.slice.index.Slice.coreopsindexIndexMutInst (T I : Type)
+def core.ops.index.IndexSliceTIInst (T I : Type)
+  (inst : core.slice.index.SliceIndex I (Slice T)) :
+  core.ops.index.Index (Slice T) I := {
+  Output := inst.Output
+  index := core.slice.index.Slice.index T I inst
+}
+
+/- Trait implementation: [core::slice::index::[T]] -/
+def core.ops.index.IndexMutSliceTIInst (T I : Type)
   (inst : core.slice.index.SliceIndex I (Slice T)) :
   core.ops.index.IndexMut (Slice T) I := {
-  indexInst := core.slice.index.Slice.coreopsindexIndexInst T I inst
+  indexInst := core.ops.index.IndexSliceTIInst T I inst
   index_mut := core.slice.index.Slice.index_mut T I inst
   index_mut_back := core.slice.index.Slice.index_mut_back T I inst
 }
 
 /- Trait implementation: [core::array::[T; N]] -/
-def core.array.Array.coreopsindexIndexInst (T I : Type) (N : Usize)
+def core.ops.index.IndexArrayIInst (T I : Type) (N : Usize)
   (inst : core.ops.index.Index (Slice T) I) :
   core.ops.index.Index (Array T N) I := {
   Output := inst.Output
@@ -485,10 +484,10 @@ def core.array.Array.coreopsindexIndexInst (T I : Type) (N : Usize)
 }
 
 /- Trait implementation: [core::array::[T; N]] -/
-def core.array.Array.coreopsindexIndexMutInst (T I : Type) (N : Usize)
+def core.ops.index.IndexMutArrayIInst (T I : Type) (N : Usize)
   (inst : core.ops.index.IndexMut (Slice T) I) :
   core.ops.index.IndexMut (Array T N) I := {
-  indexInst := core.array.Array.coreopsindexIndexInst T I N inst.indexInst
+  indexInst := core.ops.index.IndexArrayIInst T I N inst.indexInst
   index_mut := core.array.Array.index_mut T I N inst
   index_mut_back := core.array.Array.index_mut_back T I N inst
 }
@@ -532,13 +531,13 @@ def core.slice.index.Usize.index_mut_back
   sorry -- TODO
 
 /- Trait implementation: [core::slice::index::private_slice_index::usize] -/
-def core.slice.index.private_slice_index.usize.coresliceindexprivate_slice_indexSealedInst
+def core.slice.index.private_slice_index.SealedUsizeInst
   : core.slice.index.private_slice_index.Sealed Usize := {}
 
 /- Trait implementation: [core::slice::index::usize] -/
-def core.slice.index.usize.coresliceindexSliceIndexInst (T : Type) :
+def core.slice.index.SliceIndexUsizeSliceTInst (T : Type) :
   core.slice.index.SliceIndex Usize (Slice T) := {
-  sealedInst := core.slice.index.private_slice_index.usize.coresliceindexprivate_slice_indexSealedInst
+  sealedInst := core.slice.index.private_slice_index.SealedUsizeInst
   Output := T
   get := core.slice.index.Usize.get T
   get_mut := core.slice.index.Usize.get_mut T
diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean
index bbed6082..e600a151 100644
--- a/backends/lean/Base/Primitives/Vec.lean
+++ b/backends/lean/Base/Primitives/Vec.lean
@@ -153,19 +153,19 @@ def Vec.coreopsindexIndexMutInst (T I : Type)
 
 @[simp]
 theorem Vec.index_slice_index {α : Type} (v : Vec α) (i : Usize) :
-  Vec.index α Usize (core.slice.index.usize.coresliceindexSliceIndexInst α) v i =
+  Vec.index α Usize (core.slice.index.SliceIndexUsizeSliceTInst α) v i =
   Vec.index_usize v i :=
   sorry
 
 @[simp]
 theorem Vec.index_mut_slice_index {α : Type} (v : Vec α) (i : Usize) :
-  Vec.index_mut α Usize (core.slice.index.usize.coresliceindexSliceIndexInst α) v i =
+  Vec.index_mut α Usize (core.slice.index.SliceIndexUsizeSliceTInst α) v i =
   Vec.index_usize v i :=
   sorry
 
 @[simp]
 theorem Vec.index_mut_back_slice_index {α : Type} (v : Vec α) (i : Usize) (x : α) :
-  Vec.index_mut_back α Usize (core.slice.index.usize.coresliceindexSliceIndexInst α) v i x =
+  Vec.index_mut_back α Usize (core.slice.index.SliceIndexUsizeSliceTInst α) v i x =
   Vec.update_usize v i x :=
   sorry