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

feat(frontends/lean/elaborator): do not apply delayed_coercions on equation lhs

Browse source 
The variables in the equation lhs do not have type at preprocessing
time (i.e., their type is a metavariable). So, they may seem candidates
for delayed_coercions. If the coercions are injected, we will not be
able to pattern match. Thus, we disable coercions in this case.
This commit is contained in:
Leonardo de Moura 2015-01-13 17:43:14 -08:00
parent 8246feff67
commit e48df78938
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -511,7 +511,7 @@ pair<expr, constraint_seq> elaborator::ensure_has_type(
justification const & j, bool relax) {
if (is_meta(expected_type) && has_coercions_from(a_type)) {
return mk_delayed_coercion(a, a_type, expected_type, j);
} else if (is_meta(a_type) && has_coercions_to(expected_type)) {
} else if (!m_in_equation_lhs && is_meta(a_type) && has_coercions_to(expected_type)) {
return mk_delayed_coercion(a, a_type, expected_type, j);
} else {
pair<bool, constraint_seq> dcs;