diff options
| author | Son HO | 2023-09-14 08:19:59 +0200 |
|---|---|---|
| committer | GitHub | 2023-09-14 08:19:59 +0200 |
| commit | 242aca3092c6594206896ea62eb40395accc8459 (patch) | |
| tree | 4a105b1284821a89ca344188fdddb727de2deea3 /backends/lean/Base/IList | |
| parent | da97fc1e68d147439436ff883ac865a9cdeca18e (diff) | |
| parent | 743e8cb9d5366b879f53d7d0ba8adeb2f83ef72f (diff) | |
Merge pull request #36 from AeneasVerif/update_lean
Update the version of Lean and fix a bug in the progress tactic
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 |