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

feat(frontends/lean/elaborator): catch exception at is_def_eq

Browse source 
@semorrison this commit improves the bad error message you have
reported at lean-user. It is not perfect since the user has to
remember the position of the structure field in the constructor.
This commit is contained in:
Leonardo de Moura 2017-01-06 08:16:16 -08:00
parent 6f8ccb5873
commit 31a0d7d520
3 changed files with 18 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -532,7 +532,11 @@ optional<expr> elaborator::mk_coercion(expr const & e, expr e_type, expr type, e
bool elaborator::is_def_eq(expr const & e1, expr const & e2) {
type_context::approximate_scope scope(m_ctx);
return m_ctx.is_def_eq(e1, e2);
try {
return m_ctx.is_def_eq(e1, e2);
} catch (exception &) {
return false;
}
}
bool elaborator::try_is_def_eq(expr const & e1, expr const & e2) {

5
tests/lean/bad_error4.lean Normal file
View file

@ -0,0 +1,5 @@
structure foo :=
(f: unit -> unit)
definition bar : foo :=
{ f := λ a b, _ }

8
tests/lean/bad_error4.lean.expected.out Normal file
View file

@ -0,0 +1,8 @@
bad_error4.lean:5:0: error: type mismatch at application
foo.mk (λ (a : unit) (b : delayed[?m_1]), delayed[?m_2])
term
λ (a : unit) (b : delayed[?m_1]), delayed[?m_2]
has type
Π (a : unit) (b : delayed[?m_1]), delayed[?m_3]
but is expected to have type
unit → unit