From 0504acdaee98f28dfd08c5652b39c201c252d1be Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 14 Sep 2023 07:07:44 +0200
Subject: Update to Lean 4.0.0 and fix some broken proofs

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

(limited to 'backends/lean/Base/IList')

diff --git a/backends/lean/Base/IList/IList.lean b/backends/lean/Base/IList/IList.lean
index 0b483e90..a940da25 100644
--- a/backends/lean/Base/IList/IList.lean
+++ b/backends/lean/Base/IList/IList.lean
@@ -239,7 +239,6 @@ open Arith in
     have := tl.len_pos
     linarith
   else
-    simp at hineq
     have : 0 < i := by int_tac
     simp [*]
     apply hi
@@ -364,8 +363,8 @@ theorem index_itake_append_end [Inhabited α] (i j : Int) (l0 l1 : List α)
   match l0 with
   | [] => by
     simp at *
-    have := index_itake i j l1 (by simp_all) (by simp_all) (by simp_all; int_tac)
-    simp [*]
+    have := index_itake i j l1 (by simp_all) (by simp_all) (by int_tac)
+    try simp [*]
   | hd :: tl =>
     have : ¬ i = 0 := by simp at *; int_tac
     if hj : j = 0 then by simp_all; int_tac -- Contradiction
-- 
cgit v1.2.3