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

fix(library/elaborator): bug in simple_ho_match

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-15 21:48:55 -08:00
parent 19ad39159e
commit 61bd27ff06
3 changed files with 14 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/library/elaborator/elaborator.cpp
View file

@ -747,6 +747,14 @@ class elaborator::imp {
(is_eq(c) || (is_lhs && !is_actual_upper(b)) || (!is_lhs && !is_actual_lower(b))); (is_eq(c) || (is_lhs && !is_actual_upper(b)) || (!is_lhs && !is_actual_lower(b)));
} }
optional<expr> try_get_type(context const & ctx, expr const & e) {
try {
return some_expr(m_type_inferer(e, ctx));
} catch (...) {
return none_expr();
}
}
/** /**
\brief Return true iff ctx |- a == b is a "simple" higher-order matching constraint. By simple, we mean \brief Return true iff ctx |- a == b is a "simple" higher-order matching constraint. By simple, we mean
a constraint of the form a constraint of the form
@ -761,7 +769,7 @@ class elaborator::imp {
expr m = arg(a, 0); expr m = arg(a, 0);
buffer<expr> types; buffer<expr> types;
for (unsigned i = 1; i < num_args(a); i++) { for (unsigned i = 1; i < num_args(a); i++) {
optional<expr> d = lookup(ctx, var_idx(arg(a, i))).get_domain(); optional<expr> d = try_get_type(ctx, arg(a, i));
if (d) if (d)
types.push_back(*d); types.push_back(*d);
else else

2
tests/lean/elab6.lean Normal file
View file

@ -0,0 +1,2 @@
Theorem ForallIntro2 (A : Type U) (P : A -> Bool) (H : Pi x, P x) : forall x, P x :=
Abst (fun x, EqTIntro (H x))

3
tests/lean/elab6.lean.expected.out Normal file
View file

@ -0,0 +1,3 @@
Set: pp::colors
Set: pp::unicode
Proved: ForallIntro2