fix(frontends/lean/definition_cmds): copy position for equation in meta definitions

Fixes #1377.

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);

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

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