summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--tests/lean/Tutorial.lean5
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.