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

fix(frontends/lean/elaborator): problem with 'calc' proofs discussed at issue #592

Browse source
This commit is contained in:
Leonardo de Moura 2015-05-11 13:21:45 -07:00
parent 3780e03f1b
commit 3d8586088b
2 changed files with 8 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -795,7 +795,7 @@ expr elaborator::visit_typed_expr(expr const & e, constraint_seq & cs) {
constraint_seq t_cs;
expr t = visit(get_typed_expr_type(e), t_cs);
constraint_seq v_cs;
expr v = visit(get_typed_expr_expr(e), v_cs);
expr v = visit_expecting_type_of(get_typed_expr_expr(e), t, v_cs);
expr v_type = infer_type(v, v_cs);
justification j = mk_type_mismatch_jst(v, v_type, t, e);
auto new_vcs = ensure_has_type(v, v_type, t, j);

7
tests/lean/run/592.lean Normal file
View file

@ -0,0 +1,7 @@
import data.nat
open nat
definition foo (a b : nat) := a * b
example (a : nat) : foo a 0 = 0 :=
calc a * 0 = 0 : by rewrite mul_zero