From 3d8586088b2402d25f334355d4375cca870e69bf Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 11 May 2015 13:21:45 -0700 Subject: [PATCH] fix(frontends/lean/elaborator): problem with 'calc' proofs discussed at issue #592 --- src/frontends/lean/elaborator.cpp | 2 +- tests/lean/run/592.lean | 7 +++++++ 2 files changed, 8 insertions(+), 1 deletion(-) create mode 100644 tests/lean/run/592.lean diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 0e44bec93..bd1f09ebd 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -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); diff --git a/tests/lean/run/592.lean b/tests/lean/run/592.lean new file mode 100644 index 000000000..3b8584da4 --- /dev/null +++ b/tests/lean/run/592.lean @@ -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