From 266075b8a4fb9a0be922d5cd4ce61380ec4d87f2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Mon, 22 Jan 2024 20:15:48 -0800
Subject: [PATCH] chore: fix tests

---
 tests/lean/run/simproc1.lean            | 6 +++---
 tests/lean/simp_trace.lean.expected.out | 2 +-
 tests/lean/simprocTrace.lean            | 4 ++--
 3 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/tests/lean/run/simproc1.lean b/tests/lean/run/simproc1.lean
index 2c01542ca4..ec6eb08984 100644
--- a/tests/lean/run/simproc1.lean
+++ b/tests/lean/run/simproc1.lean
@@ -5,9 +5,9 @@ def foo (x : Nat) : Nat :=
 
 open Lean Meta
 
-simproc reduceFoo (foo _) := fun e => OptionT.run do
-  guard (e.isAppOfArity ``foo 1)
-  let n ← Nat.fromExpr? e.appArg!
+simproc reduceFoo (foo _) := fun e => do
+  unless e.isAppOfArity ``foo 1 do return .continue
+  let some n ← Nat.fromExpr? e.appArg! | return .continue
   return .done { expr := mkNatLit (n+10) }
 
 example : x + foo 2 = 12 + x := by
diff --git a/tests/lean/simp_trace.lean.expected.out b/tests/lean/simp_trace.lean.expected.out
index 2d4398c90b..ec8d77ce13 100644
--- a/tests/lean/simp_trace.lean.expected.out
+++ b/tests/lean/simp_trace.lean.expected.out
@@ -49,7 +49,7 @@ Try this: simp only [h, Nat.sub_add_cancel]
 Try this: simp (config := { contextual := true }) only [Nat.sub_add_cancel]
 [Meta.Tactic.simp.rewrite] h:1000, 1 ≤ x ==> True
 [Meta.Tactic.simp.rewrite] @Nat.sub_add_cancel:1000, x - 1 + 1 ==> x
-[Meta.Tactic.simp.rewrite] @eq_self:1000, (if h : 1 ≤ x then x else 0) = if _h : 1 ≤ x then x else 0 ==> True
+[Meta.Tactic.simp.rewrite] @eq_self:1000, (if h : 1 ≤ x then x else 0) = if h : 1 ≤ x then x else 0 ==> True
 Try this: simp only [and_self]
 [Meta.Tactic.simp.rewrite] and_self:1000, b ∧ b ==> b
 [Meta.Tactic.simp.rewrite] iff_self:1000, a ∧ b ↔ a ∧ b ==> True
diff --git a/tests/lean/simprocTrace.lean b/tests/lean/simprocTrace.lean
index 9ce59a2159..8a0c792586 100644
--- a/tests/lean/simprocTrace.lean
+++ b/tests/lean/simprocTrace.lean
@@ -5,8 +5,8 @@ def foo (x : Nat) : Nat :=
   x + 10
 
 simproc reduce_foo (foo _) := fun e => open Lean Meta in do
-  let some n ← evalNat e.appArg! |>.run | return none
-  return some (.done { expr := mkNatLit (n+10) })
+  let some n ← evalNat e.appArg! |>.run | return .continue
+  return .done { expr := mkNatLit (n+10) }
 
 set_option tactic.simp.trace true
 example : x + foo 2 = 12 + x := by