From 648f6c5f8205883a1941d296f4b1fab0d95dfd2e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 5 Dec 2015 19:43:48 -0800 Subject: [PATCH] fix(library/blast/strategies): constructor action was being applied too soon --- src/library/blast/strategies/simple_strategy.cpp | 2 +- tests/lean/run/blast_meta_bug.lean | 7 +++++++ 2 files changed, 8 insertions(+), 1 deletion(-) create mode 100644 tests/lean/run/blast_meta_bug.lean diff --git a/src/library/blast/strategies/simple_strategy.cpp b/src/library/blast/strategies/simple_strategy.cpp index b3f100405..125c8bd37 100644 --- a/src/library/blast/strategies/simple_strategy.cpp +++ b/src/library/blast/strategies/simple_strategy.cpp @@ -52,8 +52,8 @@ class simple_strategy_fn : public strategy_fn { Try(trivial_action()); Try(assumption_action()); Try(recursor_action()); - Try(constructor_action()); Try(ematch_action()); + Try(constructor_action()); Try(by_contradiction_action()); TryStrategy(mk_backward_strategy()); Try(qfc_action(list())); diff --git a/tests/lean/run/blast_meta_bug.lean b/tests/lean/run/blast_meta_bug.lean new file mode 100644 index 000000000..bb5dc61ff --- /dev/null +++ b/tests/lean/run/blast_meta_bug.lean @@ -0,0 +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 + +example (a : A) : P a → Exists Q := +by blast