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

feat(frontends/lean/elaborator): catch error early

Browse source
This commit is contained in:
Leonardo de Moura 2017-01-05 13:37:55 -08:00
parent b0de6723ec
commit eeab242595
3 changed files with 12 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -2725,6 +2725,7 @@ expr_pair elaborator::elaborate_with_type(expr const & e, expr const & e_type) {
{
expr Type = visit(copy_tag(e_type, mk_sort(mk_level_placeholder())), none_expr());
new_e_type = visit(e_type, some_expr(Type));
ensure_type(new_e_type, e_type);
new_e = visit(e, some_expr(new_e_type));
synthesize();
}

7
tests/lean/bad_error3.lean Normal file
View file

@ -0,0 +1,7 @@
example (p : nat → nat → Prop) : p 0 :=
begin
end
def ex (p : nat → nat → Prop) : p 0 :=
begin
end

4
tests/lean/bad_error3.lean.expected.out Normal file
View file

@ -0,0 +1,4 @@
bad_error3.lean:1:33: error: type expected at
p 0
bad_error3.lean:5:32: error: type expected at
p 0