From a73f813133815ce6b0fbf75128c3ca2bb44ce329 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 26 Jul 2016 14:49:01 -0700 Subject: [PATCH] feat(frontends/lean/elaborator): remove coercion resolution --- src/frontends/lean/elaborator.cpp | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 3aecddc76f..74ae9488b2 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -249,24 +249,24 @@ auto elaborator::use_elim_elab(name const & fn) -> optional { } expr elaborator::ensure_function(expr const & e, expr const & ref) { - // TODO(Leo): infer type and try to apply coercion to function if needed - // ref is only needed for generating error messages + expr e_type = whnf(infer_type(e)); + if (!is_pi(e_type)) { + throw_elaborator_exception(ref, format("function expected at") + pp_indent(e)); + } return e; } expr elaborator::ensure_type(expr const & e, expr const & ref) { - // TODO(Leo): infer e type, and apply coercions if needed. - // ref is only needed for generating error messages + expr e_type = whnf(infer_type(e)); + if (!is_sort(e_type)) { + throw_elaborator_exception(ref, format("type expected at") + pp_indent(e)); + } return e; } optional elaborator::ensure_has_type(expr const & e, expr const & e_type, expr const & type) { if (is_def_eq(e_type, type)) return some_expr(e); - - // TODO(Leo): try coercions - // ref is only needed for generating error messages - return none_expr(); }