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

fix(frontends/lean/elaborator): use preprocessed expression when displaying errors

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-29 14:24:12 -07:00
parent 634363c5ec
commit 320bc55e85
3 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -823,7 +823,7 @@ public:
expr a_type = instantiate_metavars(infer_type(a));
expr r = mk_app(f, a, e.get_tag());
justification j = mk_app_justification(e, a, d_type, a_type);
justification j = mk_app_justification(r, a, d_type, a_type);
expr new_a = ensure_type(a, a_type, d_type, j, m_relax_main_opaque);
return update_app(r, app_fn(r), new_a);
}
@ -1205,7 +1205,7 @@ public:
flet<bool> set_relax(m_relax_main_opaque, is_opaque && !get_hide_main_opaque(m_env));
expr r_v = visit(v);
expr r_v_type = infer_type(r_v);
justification j = mk_justification(v, [=](formatter const & fmt, substitution const & subst) {
justification j = mk_justification(r_v, [=](formatter const & fmt, substitution const & subst) {
substitution s(subst);
return pp_def_type_mismatch(fmt, n, s.instantiate(r_t), s.instantiate(r_v_type));
});

2
tests/lean/calc1.lean.expected.out
View file

@ -1,4 +1,4 @@
le_eq_trans a d e (le_trans a c d (eq_le_trans a b c H1 H2) H3) H4 : le a e
calc1.lean:38:10: error: invalid 'calc' expression, transitivity rule is not defined for current step
le_lt_trans b c d H2 H5 : lt b d
[choice ([@ le2_trans] b d e ([@ le2_trans] b c d H2 H3) H4) ([@ le_trans] b d e ([@ le_trans] b c d H2 H3) H4)]
[choice (@le2_trans b d e (@le2_trans b c d H2 H3) H4) (@le_trans b d e (@le_trans b c d H2 H3) H4)]

2
tests/lean/crash.lean.expected.out
View file

@ -1,6 +1,6 @@
crash.lean:8:12: error: type mismatch at application
have H' : not P, from H,
_
?M_1 P H
term
H
is expected of type