michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/blast/forward/pattern): pattern inference bug

Browse source
This commit is contained in:
Leonardo de Moura 2015-12-05 19:38:24 -08:00
parent ae8efb684e
commit 20d7727a9c
3 changed files with 8 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/blast/forward/pattern.cpp
View file

@ -550,9 +550,9 @@ struct mk_hi_lemma_fn {
lean_assert(m_mvars.size() == inst_implicit_flags.size()); lean_assert(m_mvars.size() == inst_implicit_flags.size());
buffer<expr> subst; buffer<expr> subst;
buffer<expr> residue_locals; buffer<expr> residue_locals;
candidate_set hints = collect_pattern_hints(m_mvars, B);
expr proof = mk_proof(residue_locals, subst); expr proof = mk_proof(residue_locals, subst);
B = replace_mvars(B, subst); B = replace_mvars(B, subst);
candidate_set hints = collect_pattern_hints(m_mvars, B);
list<multi_pattern> mps; list<multi_pattern> mps;
if (!hints.empty()) { if (!hints.empty()) {
mps = mk_multi_patterns_using(hints, false); mps = mk_multi_patterns_using(hints, false);

3
tests/lean/pattern_bug1.lean Normal file
View file

@ -0,0 +1,3 @@
constants {A : Type} (P : A → Prop) (R : A → A → Prop)
definition H [forward] : ∀ a, (: P a :) → ∃ b, R a b := sorry
print H

4
tests/lean/pattern_bug1.lean.expected.out Normal file
View file

@ -0,0 +1,4 @@
definition H [forward] : ∀ (a : A), (:P a:) → Exists (R a) :=
sorry
(multi-)patterns:
{P ?M_1}