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

fix(frontends/lean/elaborator): fixes #719

Browse source
This commit is contained in:
Leonardo de Moura 2015-07-03 12:37:28 -07:00
parent aa2a5b6282
commit c843690d27
2 changed files with 17 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/frontends/lean/elaborator.cpp
View file

@ -286,6 +286,9 @@ expr elaborator::visit_expecting_type(expr const & e, constraint_seq & cs) {
expr r = m_context.mk_type_meta(m_ngen, e.get_tag());
save_placeholder_info(e, r);
return r;
} else if (is_no_info(e)) {
flet<bool> let(m_no_info, true);
return visit_expecting_type(get_annotation_arg(e), cs);
} else {
return visit(e, cs);
}
@ -297,6 +300,9 @@ expr elaborator::visit_expecting_type_of(expr const & e, expr const & t, constra
expr r = mk_placeholder_meta(some_expr(t), e.get_tag(), is_strict_placeholder(e), inst_imp, cs);
save_placeholder_info(e, r);
return r;
} else if (is_no_info(e)) {
flet<bool> let(m_no_info, true);
return visit_expecting_type_of(get_annotation_arg(e), t, cs);
} else if (is_choice(e)) {
return visit_choice(e, some_expr(t), cs);
} else if (is_by(e)) {

11
tests/lean/hott/719.hlean Normal file
View file

@ -0,0 +1,11 @@
-- HoTT
open eq
variables {A A' : Type} {a a' : A} {C : A → A' → Type} (p : a = a') (f : Π(b : A'), C a b) (b : A')
definition foo : (transport _ p f) b = p ▸ (f b) := sorry
definition bar : (p ▸ f) b = transport _ p (f b) := sorry
definition bla : (p ▸ f) b = p ▸ (f b) := sorry