diff options
Diffstat (limited to 'backends/lean/Base/IList/IList.lean')
| -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 |