fix test

Author: kim-em

MathlibTest/toAdditive.lean

@@ -180,9 +180,8 @@ example {x} (h : 1 = x) : baz20 = x := by simp; guard_target = 1 = x; exact h
 @[to_additive bar21]
 def foo21 {N} {A} [Pow A N] (a : A) (n : N) : A := a ^ n
 
-run_meta do
-  let some ⟨`Test.bar21, r, .arg 1⟩ := translations.find? (← getEnv) `Test.foo21 | failure
-  guard <| r.isEmpty
+run_meta guard <| translations.find? (← getEnv) `Test.foo21
+  matches some ⟨`Test.bar21, ⟨[], ⟨[], #[]⟩⟩, .arg 1⟩
 
 @[to_additive bar22]
 abbrev foo22 {α} [Monoid α] (a : α) : ℕ → α
@@ -838,10 +837,9 @@ instance : Mul (MonoidAlgebra Nat G) where
 def monoidAlgebraFoo {k G : Type} [Inhabited k] : MonoidAlgebra k G × Nat :=
   (⟨fun _ ↦ default⟩, 2)
 
-run_meta do
-  let some ⟨``addMonoidAlgebraFoo, r, .arg 1⟩ := translations.find? (← getEnv) ``monoidAlgebraFoo
-    | failure
-  guard <| r.isEmpty
+run_meta guard <|
+  translations.find? (← getEnv) ``monoidAlgebraFoo
+    matches some ⟨``addMonoidAlgebraFoo, ⟨[], ⟨[], #[]⟩⟩, .arg 1⟩
 
 /--
 warning: `to_additive` correctly autogenerated `(relevant_arg := 2)` for `monoidAlgebraFoo₁`.