From 63ee3b1bc65b67aeed843f052d7f67c9f3c0ab89 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 2 Feb 2024 23:16:57 +0100
Subject: Start fixing the tests

---
 tests/lean/Tutorial.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tests/lean/Tutorial.lean')

diff --git a/tests/lean/Tutorial.lean b/tests/lean/Tutorial.lean
index 840a606e..d92b2dd7 100644
--- a/tests/lean/Tutorial.lean
+++ b/tests/lean/Tutorial.lean
@@ -376,7 +376,7 @@ theorem i32_id_spec (x : I32) (h : 0 ≤ x.val) :
 --
 -- We first specify a decreasing value. Here, we state that [x], seen as a natural number,
 -- decreases at every recursive call.
-termination_by i32_id_spec x _ => x.val.toNat
+termination_by x.val.toNat
 -- And we now have to prove that it indeed decreases - you can skip this for now.
 decreasing_by
   -- We first need to "massage" the goal (in practice, all the proofs of [decreasing_by]
-- 
cgit v1.2.3