From c3b6ad3685995b3b96dc88789e8512560d3257b3 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 21 Nov 2023 10:23:14 +0100
Subject: Update the standard libraries

---
 backends/lean/Base/Primitives/Vec.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'backends/lean/Base/Primitives/Vec.lean')

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
 
-- 
cgit v1.2.3