From 65a77968d0abc2d01da92aa8982256855e7519a6 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 5 Apr 2024 14:04:25 +0200
Subject: Update the lean toolchain and fix the proofs

---
 backends/lean/Base/Primitives/ArraySlice.lean | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

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

diff --git a/backends/lean/Base/Primitives/ArraySlice.lean b/backends/lean/Base/Primitives/ArraySlice.lean
index e1a39d40..3bd2aebb 100644
--- a/backends/lean/Base/Primitives/ArraySlice.lean
+++ b/backends/lean/Base/Primitives/ArraySlice.lean
@@ -2,7 +2,6 @@
 import Lean
 import Lean.Meta.Tactic.Simp
 import Init.Data.List.Basic
-import Mathlib.Tactic.RunCmd
 import Mathlib.Tactic.Linarith
 import Base.IList
 import Base.Primitives.Scalar
@@ -269,7 +268,7 @@ def Array.update_subslice (α : Type u) (n : Usize) (a : Array α n) (r : Range
       . scalar_tac
       . scalar_tac
     let na := s_beg.append (s.val.append s_end)
-    have : na.len = a.val.len := by simp [*]
+    have : na.len = a.val.len := by simp [na, *]
     ret ⟨ na, by simp_all [← List.len_eq_length]; scalar_tac ⟩
   else
     fail panic
@@ -343,7 +342,7 @@ def Slice.update_subslice (α : Type u) (s : Slice α) (r : Range Usize) (ss : S
       . scalar_tac
       . scalar_tac
     let ns := s_beg.append (ss.val.append s_end)
-    have : ns.len = s.val.len := by simp [*]
+    have : ns.len = s.val.len := by simp [ns, *]
     ret ⟨ ns, by simp_all [← List.len_eq_length]; scalar_tac ⟩
   else
     fail panic
-- 
cgit v1.2.3