max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(frontends/lean/elaborator): remove coercion resolution

Browse source
This commit is contained in:
Leonardo de Moura 2016-07-26 14:49:01 -07:00
parent 83d4436079
commit a73f813133
1 changed files with 8 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -249,24 +249,24 @@ auto elaborator::use_elim_elab(name const & fn) -> optional<elim_info> {
}
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<expr> 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();
}