From e48df78938d743c471bcacefbd4946ce1d6efc46 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 13 Jan 2015 17:43:14 -0800 Subject: [PATCH] feat(frontends/lean/elaborator): do not apply delayed_coercions on equation lhs 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. --- src/frontends/lean/elaborator.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 0b19ea1ab..3ad60ca03 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -511,7 +511,7 @@ pair 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 dcs;