From c06ca8304d2f1078dfb43e5862ceee12a8147afb Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 18 Feb 2021 16:54:45 -0800
Subject: [PATCH] fix: test

---
 tests/lean/run/simp1.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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