diff options
| author | Son Ho | 2023-09-14 07:07:44 +0200 |
|---|---|---|
| committer | Son Ho | 2023-09-14 07:07:44 +0200 |
| commit | 0504acdaee98f28dfd08c5652b39c201c252d1be (patch) | |
| tree | 0ba96dd2a488e0cb98442ad67030f0e637b9670b /backends/lean/Base/IList | |
| parent | da97fc1e68d147439436ff883ac865a9cdeca18e (diff) | |
Update to Lean 4.0.0 and fix some broken proofs
Diffstat (limited to 'backends/lean/Base/IList')
| -rw-r--r-- | backends/lean/Base/IList/IList.lean | 5 |
1 files changed, 2 insertions, 3 deletions
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 |