From 0c2878e509710bf0ebf7f087d0cb3f718c3102bf Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Fri, 17 Feb 2017 20:57:12 +0100
Subject: [PATCH] fix(frontends/lean/definition_cmds): copy position for
 equation in meta definitions

Fixes #1377.
---
 src/frontends/lean/definition_cmds.cpp         | 2 +-
 tests/lean/meta_equation_pos.lean              | 4 ++++
 tests/lean/meta_equation_pos.lean.expected.out | 8 ++++++++
 3 files changed, 13 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/meta_equation_pos.lean
 create mode 100644 tests/lean/meta_equation_pos.lean.expected.out

diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp
index 4b13e9e302..f79c1393c4 100644
--- a/src/frontends/lean/definition_cmds.cpp
+++ b/src/frontends/lean/definition_cmds.cpp
@@ -186,7 +186,7 @@ static expr_pair parse_definition(parser & p, buffer<name> & lp_names, buffer<ex
             p.add_local(fn);
             val = p.parse_expr();
             /* add fake equation */
-            expr eqn = mk_equation(fn, val);
+            expr eqn = copy_tag(val, mk_equation(fn, val));
             buffer<expr> eqns;
             eqns.push_back(eqn);
             val = mk_equations(p, fn, scope2.get_name(), eqns, {}, header_pos);
diff --git a/tests/lean/meta_equation_pos.lean b/tests/lean/meta_equation_pos.lean
new file mode 100644
index 0000000000..9b1d7f2dd7
--- /dev/null
+++ b/tests/lean/meta_equation_pos.lean
@@ -0,0 +1,4 @@
+meta def f (x : nat) : nat :=
+tt -- type error should be reported here
+
+check nat
diff --git a/tests/lean/meta_equation_pos.lean.expected.out b/tests/lean/meta_equation_pos.lean.expected.out
new file mode 100644
index 0000000000..b858f7a35c
--- /dev/null
+++ b/tests/lean/meta_equation_pos.lean.expected.out
@@ -0,0 +1,8 @@
+meta_equation_pos.lean:2:0: error: equation type mismatch, expression
+  tt
+has type
+  bool
+but is expected to have type
+  ℕ
+meta_equation_pos.lean:1:9: warning: declaration 'f' uses sorry
+ℕ : Type