diff options
| author | Son Ho | 2023-09-18 13:07:02 +0200 |
|---|---|---|
| committer | Son Ho | 2023-09-18 13:07:02 +0200 |
| commit | 985277c435feaafcdb034cd51ff113d67b9304a6 (patch) | |
| tree | fe0963c0977241bad2df4f24f6c965aebe46e3ba /tests/lean/Tutorial.lean | |
| parent | ba215d5f7f2cd087e6b920e7ea1793e4b114a775 (diff) | |
Make minor modifications to the tutorial
Diffstat (limited to 'tests/lean/Tutorial.lean')
| -rw-r--r-- | tests/lean/Tutorial.lean | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/tests/lean/Tutorial.lean b/tests/lean/Tutorial.lean index 0ba830a6..55bddd03 100644 --- a/tests/lean/Tutorial.lean +++ b/tests/lean/Tutorial.lean @@ -335,13 +335,12 @@ theorem i32_id_spec (x : I32) (h : 0 ≤ x.val) : simp_all else simp [hx] - -- TODO: automatic lookup doesn't work? -- x - 1 - progress with Scalar.sub_spec as ⟨ x1 ⟩ + progress as ⟨ x1 ⟩ -- Recursive call progress as ⟨ x2 ⟩ -- x2 + 1 - progress with Scalar.add_spec + progress -- Postcondition simp; scalar_tac -- Below: we have to prove that the recursive call performed in the proof terminates. |