diff --git a/tests/lean/run/simp1.lean b/tests/lean/run/simp1.lean index a95e467228..61fe508cee 100644 --- a/tests/lean/run/simp1.lean +++ b/tests/lean/run/simp1.lean @@ -46,7 +46,8 @@ def tst2 : MetaM Unit := do let s ← Meta.getSimpLemmas let m ← s.post.getMatch lhs trace[Meta.debug]! "result: {m}" - assert! m.size == 3 + assert! m.any fun s => s.name? == `ex2 + set_option trace.Meta.debug true in #eval tst2