1 files changed, 19 insertions, 20 deletions
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