diff --git a/tests/lean/run/blast_meta_bug.lean b/tests/lean/run/blast_meta_bug.lean index bb5dc61ff..ca6e04f1b 100644 --- a/tests/lean/run/blast_meta_bug.lean +++ b/tests/lean/run/blast_meta_bug.lean @@ -1,7 +1,7 @@ constants {A : Type.{1}} (P : A → Prop) (Q : A → Prop) definition H : ∀ a, (: P a :) → Exists Q := sorry -set_option blast.ematch true +set_option blast.strategy "ematch" example (a : A) : P a → Exists Q := by blast